---

Step * of Lemma CRX-protocol-legal

∀s:SES
  Legal([CR-initiator1{i:l}(s);
         CR-initiator2{i:l}(s);
         CR-initiator4{i:l}(s);
         CR-responder4{i:l}(s);
         CR-responder5{i:l}(s);
         CR-responder6{i:l}(s)])
BY
{ ProveProtocolLegal⋅ }

---

Latex:

---

Latex:
\mforall{}s:SES
    Legal([CR-initiator1\{i:l\}(s);
                  CR-initiator2\{i:l\}(s);
                  CR-initiator4\{i:l\}(s);
                  CR-responder4\{i:l\}(s);
                  CR-responder5\{i:l\}(s);
                  CR-responder6\{i:l\}(s)])


By

---

Latex:
ProveProtocolLegal\mcdot{}

---

Home Index