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"
Thanks to Amine.
This archive was generated by a fusion of
Pipermail (Mailman edition) and