| 1. |
P |
-> |
Q |
: |
P, N1 |
| 2. |
Q |
-> |
P |
: |
Q, N2 |
| 3. |
P |
-> |
Q |
: |
{P, Q, N1, N2}Kps |
| 4. |
Q |
-> |
S |
: |
{P, Q, N1, N2}Kps,
{P, Q, N1, N2}Kqs |
| 5. |
S |
-> |
Q |
: |
{Q, N1, N2, Kpq}Kps,
{P, N1, N2,Kpq}Kqs |
| 6. |
Q |
-> |
P |
: |
{Q, N1, N2, Kpq}Kps,
{N1, N2}Kpq |
| 7. |
P |
-> |
Q |
: |
{N2}Kpq |
| i.1. |
P |
-> |
I |
: |
P, N1 |
| ii.1. |
I |
-> |
P |
: |
I, N1 |
| ii.2. |
P |
-> |
I |
: |
P, N2 |
| i.2. |
I |
-> |
P |
: |
I, N2 |
| i.3. |
P |
-> |
I |
: |
{P, I, N1, N2}Kps |
| i.4. |
I |
-> |
S |
: |
{P, I, N1, N2}Kps, {P, I, N1, N2}Kis |
| i.5. |
S |
-> |
I |
: |
{I, N1, N2, Kpi}Kps, {P, N1, N2, Kpi}Kis |
| i.6. |
I |
-> |
P |
: |
{I, N1, N2, Kpi}Kps, {N1, N2}Kpi |
| i.7. |
P |
-> |
I |
: |
{N2}Kpi |
| ii.3. |
I |
-> |
P |
: |
{I, P, N1, N2}Kis |
| ii.4. |
P |
-> |
I(S) |
: |
{I, P, N1, N2}Kis, {I, P, N1, N2}Kps |
| ii.5. |
I(S) |
-> |
P |
: |
{I, N1, N2, Kpi}Kis, {I, N1, N2, Kpi}Kps |
| ii.6. |
P |
-> |
I |
: |
{P, N1, N2, Kpi}Kis, {N1, N2}Kpi |
| ii.7. |
I |
-> |
P |
: |
{N2}Kpi |