なんじゃこりゃ

id:kosakにAmbient Calculusとやらの問題を押し付けられた。

!a[P]から始めて、状態遷移を繰り返した場合に、任意の自然数nに対し、途中で
a[ (n個の"a[") 0 (n個の"]") | P] | !a[P]という形のプロセスに遷移可能となるような、
プロセスPを1つ求め、実際にこのような形のプロセスに遷移可能であることを証明せよ。

とりあえずPをin a.0にしたらうまくいくような気がする。
証明はnに関する帰納法で
(i)

!a[P] -> a[P] | !a[P]
      -> a[P|0] | !a[P]
      -> a[0|P] | !a[P]

(ii)

!a[P] -> ... -> a[ (n-1個の"a[") 0 (n-1個の"]") | P] | !a[P]
を仮定すると
!a[P] -> ... -> a[ (n-1個の"a[") 0 (n-1個の"]") | in a.0] | !a[P]
      -> a[in a.0 | (n-1個の"a[") 0 (n-1個の"]") ] | !a[P]
      -> !a[P] | a[in a.0 | (n-1個の"a[") 0 (n-1個の"]") ]
      -> (a[P] | !a[P]) | a[in a.0 | (n-1個の"a[") 0 (n-1個の"]") ]
      -> a[in a.0 | (n-1個の"a[") 0 (n-1個の"]") ] | (a[P] | !a[P])
      ->(a[in a.0 | (n-1個の"a[") 0 (n-1個の"]") ] | a[P]) | !a[P]
      -> a[a[0 | (n-1個の"a[") 0 (n-1個の"]") ] | P] | !a[P]
      -> a[a[ (n-1個の"a[") 0 (n-1個の"]") | 0] | P] | !a[P]
      -> a[ (n個の"a[") 0 (n個の"]") | P] | !a[P]