1. |
C |
-> |
AS |
: |
C, S, N1 |
2. |
AS |
-> |
C |
: |
AS, {AS, C, N1, S, pk(S)}sk(AS) |
3. |
C |
-> |
S |
: |
C, S, {C, T, L, {N2}pk(S)}sk(C) |
4. |
S |
-> |
AS |
: |
S, C, N3 |
5. |
AS |
-> |
S |
: |
AS, {AS, S, N3, C, pk(C)}sk(AS) |
6. |
S |
-> |
C |
: |
S, C, {S, inc(N2)}pk(C) |
1. |
C |
-> |
AS |
: |
C, S, N1 |
2. |
AS |
-> |
C |
: |
AS, {AS, C, N1, S, pk(S)}sk(AS) |
3. |
C |
-> |
I(S) |
: |
C, S, {C, T, L, {N2}pk(S)}sk(C) |
3. |
I |
-> |
S |
: |
I, S, {I, T, L, {N2}pk(S)}sk(I) |
4. |
S |
-> |
AS |
: |
S, I, N3 |
5. |
AS |
-> |
S |
: |
AS, {AS, S, N3, I, pk(I)}sk(AS) |
6. |
S |
-> |
I |
: |
S, I, {S, inc(N2)}pk(I) |
1. |
I |
-> |
AS |
: |
I, C, N1' |
2. |
AS |
-> |
I |
: |
AS, {AS, I, N1', C, pk(C)}sk(AS) |
6. |
I(S) |
-> |
C |
: |
S, C, {S, inc(N2)}pk(C) |