# Re: [isabelle] Partial Linear Arithmetic

`P.S.: I still did not find the correct formula for the modular case,
``sample2.html. Isabelle declines to solve the lemma. Does anyone know,
``what's wrong there?
`

The "lemma" on your web page
lemma sample2: "(EX j::nat.(ALL r::int.(r-2*j<=1)))"

`is not even syntactically well-formed, has a type problem (nat/int) and
``is definitely false. Your purported solution "j=2 dvd (r)" does not make
``sense because your quantifiers are in the wrong order. If you swap them
``and correct all the mistakes, it works:
`
lemma sample2: "ALL r::int. EX j. r - 2*j<=1"
by arith
Thanks to Amine.
Tobias

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