Sejam P e Q schemas equivalentes. Para mostrar a equivalência entre estes schemas usando Z/Eves deve ser provado o predicado:
P \iff Q
Uma forma tipica de mostrar esta equivalência é dividi-la em duas partes:
1. P \implies Q
2. Q \implies P
Para transformar o predicado P \iff Q nos predicados 1 e 2, o usuário pode entrar com os seguintes comandos de prova:
slip P
rewrite
cases
rewrite
Neste ponto o predicado 1 foi obtido.
next
split Q
rewrite
Neste ponto o predicado 2 foi obtido.
Agora, é somente provar os predicados. Para alternar entre eles utiliza-se o comando next.
Assinar:
Postar comentários (Atom)
Um comentário:
Cara, muito bacana que você tenha um blog sobre essa assunto. Estou começando a estudar, então pode ter certeza que pelo menos você terá alguém para discutir o assunto sempre contigo...
PS: se não fosse pela foto eu nem ia te reconhecer...
Abração,
Michel (caso não lembre, seu colega de sala de aula de metodos formais)
Postar um comentário