# [isabelle] Infinitely recursive lambda expression or not?

`My ashamed apologizes if this looks as weird as I'm afraid it may looks,
``however, this question really tickles me.
`

`I came to something like this after some simplifications, so I wanted to
``test it with a lemma:
`
lemma "f = (λa. a ∨ f a) ⟹ (f a = a)"

`Isabelle tells me it found a counter example with “a = False” and “f a =
``True” . It does not seems to see there is an infinite recursion, or else I
``don't understand how it can believe “f a” may differs from “a” (how so?).
`

`To me, it can only be “a”, an infinite never ending sequence of
``disjunctions of the same term may be nothing else if it's ever something,
``than this term.
`

`I guess this case looks weird, but I would like to know, first if Isabelle
``sees it as an infinitely recursive lambda expression or not, then if if it
``do, if there exists some trusted axioms which are able to deal with this?
`
--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*