How to prove (p^q) ^ ( q -> r ) <-> r using Z- notation?

Question

I am trying to prove logical expressions using Z-notations. But, I am new to the Z language. Please help me to prove the above logical expression.

Answer 1

Let's do it using Z notation language which is used as a language for formal specifiaction.

1st Step : Introduction of Conjunction

(p ∧ q) ∧ ( q⇒r)  [ ∧ - elim2]   

2nd Step: We will have:

 q ⇒ r  

3rd step: We want get q is true:

p ∧ q     [ ∧ - elim2]
------
   q

4th step: Using q and q=>r we can say that r is true.

For futher information please refer to this book "using Z".