K      L      M
A ---> B ---> C ---> D
       +----> F
         L

A<B K@AB=L@BC        A<B K@AB=L@BF
A>C L@BC=K@AC        A>F L@BF=K@AF
B<C L@BC=Exported    B<F L@BF=Exported

B>C L@BC=K@AB        B>F L@BF=K@AB
A<C K@AB=K@AC        A<F K@AB=K@AF
A>B K@AB=Exported    A>B K@AB=Exported


  B<C L@BC=M@CD       + C>D M@CD-Removed
A<B K@AB=L@BC       + | K@AB=L@BC=M@CD
  B>D M@CD=L@BD     | | K@AB=L@BC=M@CD=L@BD      +L@BD
A>C L@BC=K@AC       | | K@AB=L@BC=M@CD=L@BD=K@AC +K@AC
  C<D M@CD=Exported | +
B<C L@BC=Exported   + B>C L@BC-Removed

A<B K@AB=L@BC       + B>C L@BC-Removed
  B<C L@BC=M@CD     | + K@AB=L@BC=M@CD
A>C L@BC=K@AC       | | K@AB=L@BC=M@CD=K@AC      +K@AC
  B>D M@CD=L@BD     | | K@AB=L@BC=M@CD=K@AC=L@BD +L@BD
B<C L@BC=Exported   + |
  C<D M@CD=Exported   + C>D M@CD-Removed


A<B K(@AB)=L@(B)C    B<C L(@BC)=M@(C)D    C<D M(@CD)=N@(D)E
A>C L@B(C)=K(@AC)    A<B K(@AB)=M@CD      B<C L(@BC)=N@DE
B<C L(@BC)=Exported  A>D M@C(D)=K(@AD)    A<B K(@AB)=N@DE
                     C<D M(@CD)=Exported  A>E N@D(E)=K(@AE)

A<B K(@AB)=L@(B)C    B<C L(@BC)=M@(C)D    C<D M(@CD)=N@(D)E
A>C L@B(C)=K(@AC)    A<B K(@AB)=M@CD      C>D M(@CD)=Exportin
B<C L(@BC)=Exported  A>D M@C(D)=K(@AD)    A<D K(@AD)=N@DE
                     C<D M(@CD)=Exported  A>E N@D(E)=K(@AE)
                                          D<E N(@DE)=Exported

A<B K(@AB)=L@(B)C
A<B K(@AB)=Remove    B<C L(@BC)=M@(C)D    C<D M(@CD)=N@(D)E
A>C L@B(C)=K(@AC)    B>C L(@BC)=Exportin  B<C L(@BC)=N@DE
B<C L(@BC)=Exported  A<C K(@AC)=M@(C)D    A<C K(@AC)=N@DE
                     A>D M@C(D)=K(@AD)    A>E N@D(E)=K(@AE)
                     C<D M(@CD)=Exported  D<E N(@DE)=Exported


closed:
  open+ -> +open*
  open- -> -open*
+open* K:
  +bind K -> +closing K
  -fuse K L -> +opening KL
  -remove K -> closed K
-open* K:
  -bind K -> closed K
  +fuse K L -> +exporting L
  +remove K -> -closing K
  +export K -> -closing K
+closing K:
  -fuse K L -> +closing KL
  -remove K -> closed K
-closing K:
  -bind K -> closed K
  -remove K -> closed K
+exporting L:
  -fuse L M -> +closing LM / +forward KLM / 
  -remove L -> exporting L
  -export L -> closed L


IO
bound
fused
removed

NS
wrap
unwrap
remove
fuse
bind

T
id
var
close
remove
fuse
bind

+D
bind     -> bound
fuse +D1 -> (D=D1)
fuse -D1 -> exporting +D
remove   -> !! +D removed !!

-D
bind     -> !! -D bound !!
fuse +D1 -> D=D1
fuse -D1 -> !! -D & -D1 fused !!
remove   -> removed



A ---> B <--- C
   K       L

A <--- B ---> C
    K     L



A ---> B ---> C
   K      L

A>B K=[]
B<A K=[]

A>C K@B=[]
C<A K@B=[]

B>A K=L@C    NG(C<B L=[])    open*(-K), indirectly_exporting(+L)
A<B K=L@C     |              opened(+K)
A>C L@B=[]    |
C<A L@B=[]    |
C>B L=_       |              closing(-L)
B<C L=_       +              indirectly_exporting(+L)->closed
B>C L=_
C<B L=_                      closed(-L)

B>A K=L@C    NG(C<B L=[])    open*(-K), indirectly_exporting(+L)
A<B K=L@C     |              opened(+K)
A>C L@B=L'    |              opening(+L')
C<A L@B=L'    |              opened(-L')
C>B L=_       |              closing(-L)
B<C L=_       +              indirectly_exporting(+L)->closed
B>C L=_
C<B L=_                      closed(-L)

B>A K=L@C    NG(C<B L=[])    open*(-K), indirectly_exporting(+L)
A<B K=L@C     |              opened(+K)
A>C L@B=L'    |              opening(+L')
C<A L@B=L'    |              opened(-L')
A>C L'=[]     |              closing(+L')
C<A L'=[]     |              closed(-L')
C>B L=_       |              closing(-L)
B<C L=_       +              indirectly_exporting(+L)->closed
B>C L=_
C<B L=_                      closed(-L)

B>C L=K@A    NG(A<B K=_)     open*(+L), indirectly_exporting(-K)
C<B L=K@A     |              opened(-L)
C>A K@B=K'    |              opening(-K')
A<C K@B=K'    |              opened(+K')
A>B K=[]      |              closing(+K)
B<A K=[]      +              indirectly_exporting(-K)->closed
B>A K=_
A<B K=_                      closed(+K)

B>C L=K@A    NG(A<B K=_)     open*(+L), indirectly_exporting(-K)
C<B L=K@A     |              opened(-L)
C>A K@B=K'    |              opening(-K')
A<C K@B=K'    |              opened(+K')
A>B K=_       |              closing(+K)
B<A K=_       +              indirectly_exporting(-K)->closed
B>A K=_
A<B K=_                      closed(+K)

B>C L=K@A    NG(A<B K=_)     open*(+L), indirectly_exporting(-K)
C<B L=K@A     |              opened(-L)
C>A K@B=K'    |              opening(-K')
A<C K@B=K'    |              opened(+K')
A>B K=_       |              closing(+K)
B<A K=_       +              indirectly_exporting(-K)->closed
A>B K=[]
B<A K=[]
B>A K=_
A<B K=_                      closed(+K)

B>C L=K@A    NG(A<B K=_)     open*(+L), indirectly_exporting(-K)
C<B L=K@A     |              opened(-L)
A>B K=[]      |              closing(+K)
B<A K=[]      |              indirectly_exporting(-K)
C>A K@B=K'    |              opening(-K')
A<C K@B=K'    |              opened(+K')
A>C K'=[]     |              closing(+K')
C<A K'=[]     |              closed(-K')
A>B K=_       |              closing(+K)
B<A K=_       +              indirectly_exorting(-K)->closed
B>A K=_
A<B K=_                      closed(+K)


N から X@M= を受け取ったら M へ X=_ を送る


open*->indirectly_exporting  第三者へ輸出
indirectly_exporting->closed  removeMessage を受け取る

closing->indirectly_exporting  あり得ない
closed->indirectly_exporting  あり得ない
indirectly_exporting->open*  あり得ない
indirectly_exporting->closing  あり得ない



append(X,Y,^Z)


append(X,Y,Z) :- Z=^(Z1) |
  append1(X,Y,Z1).

append1(X,Y,Z) :- X=[] |
  Z=[].
append1(X,Y,Z) :- X=[A|X1] |
  Z=[A|Z1],
  append1(X1,Y,Z1).


Sock=[chat(I,^O)|Sock1],

serv(Sock) :- Sock=[chat(I,^O)|Sock1] |
  chat(I,O),
  serv(Sock1).

chat(I,O) :- I=[] |
  O=[].
chat(I,O) :- I=[L|I1] |
  O=[L|O1],
  chat(I1,O1).


append(X,Y,^Z) :- X=[] |
  Z=Y.
append(X,Y,^Z) :- X=[A|X1] |
  Z=[A|Z1],
  append(X1,Y,^Z1).

chat(I,^O) :- I=[] |
  O=[].
chat(I,^O) :- I=[L|I1] |
  O=[L|O1],
  chat(I1,^O1).