# Re: [isabelle] about th proof of protocol

```
```
Another good exercise to understand why things happens in the proofs is to enable the Traces (simplifier and unification) in Isabelle.
```
This doubt you had is easy to grasp from the simplifier trace.

Jean

Tjark Weber escreveu:
```
```Jean,

On Wednesday 14 May 2008 05:18, jwang whu.edu.cn (jwang) wrote:
```
```The first subgoal is "[A /<not in> bad;B /<not in> bad]=>Say A B (Crypt(pubK
B){Nonce NA,Agent A})</in>set [ ]-->Nonce  NA /<not in> a nalz(knows  Spy
[]).  I can't understand  how the subgoal is proved.  I think the first
subgoal is not tenable because "Say A B (Crypt(pubK B){Nonce NA,Agent A})"
```
```
```
I haven't looked at the Isabelle proof, but your e-mail suggests that "Say A B (Crypt(pubK B){Nonce NA,Agent A})</in>set [ ]" occurs as the premise of an implication "-->" in this subgoal. Because this premise is false, the implication is trivially true.
```
Best,
Tjark

```
```

```

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