Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] how to get start to prove function of functio...


view this post on Zulip Email Gateway (Aug 22 2022 at 11:04):

From: Mandy Martin <tesleft@hotmail.com>
Hi,
I am searching for the basic axioms for function of functionsearching for axioms equivalent as basic as identity, symmetric and transitive.for example f(f(x,y),y) + f(x,f(x,y) > .... etc
so far , i have no idea about the structure of axioms, but can only use mind to think randomly such asf(f(x,y),y) + f(y,f(y,z)) > f(f(x,y),z)
would like to get start to search and prove function of function axioms in Isabelle.
Regards,
Martin


Last updated: Apr 25 2024 at 04:18 UTC