\u3053\u306e\u30c9\u30ad\u30e5\u30e1\u30f3\u30c8\u306f\u64cd\u4f5c\u4f8b\u3092\u793a\u3057\u3066\u3044\u307e\u3059. lambda> \u306f\u30d7\u30ed\u30f3\u30d7\u30c8\u8a18\u53f7\u3067\u3059.
\u578b\u306a\u3057\u30e9\u30e0\u30c0\u8a08\u7b97\u3092\u5b66\u7fd2\u3059\u308b\u969b\u306e\u53c2\u8003\u306b\u3057\u3066\u304f\u3060\u3055\u3044.
    ---------------------------------------------------------
    \u30e9\u30e0\u30c0\u8a18\u53f7\u306f\u30d0\u30c3\u30af\u30b9\u30e9\u30c3\u30b7\u30e5(\)\u3067\u8868\u3055\u308c\u3066\u3044\u307e\u3059.
    \u30de\u30af\u30ed\u53c2\u7167\u306f <true> \u306e\u3088\u3046\u306a\u8a18\u53f7\u3067\u8868\u3055\u308c\u3066\u3044\u307e\u3059.
       (\u30de\u30af\u30ed\u3068\u306f\u5358\u306a\u308b\u6587\u5b57\u5217\u7f6e\u63db\u3067\u3059.)
    \u8a73\u7d30\u306f :? \u3067\u8868\u793a\u3055\u308c\u308b\u30d8\u30eb\u30d7\u30e1\u30c3\u30bb\u30fc\u30b8\u3092\u53c2\u7167\u3057\u3066\u304f\u3060\u3055\u3044.
    ---------------------------------------------------------

\u5185\u5bb9\u306e\u4e00\u89a7
----------
  \u7c21\u7d04\u624b\u9806\u306b\u3088\u308a\u505c\u6b62\u3057\u306a\u3044\u4f8b
  \u505c\u6b62\u3057\u306a\u3044\u4f8b \u305d\u306e\uff11
  \u505c\u6b62\u3057\u306a\u3044\u4f8b \u305d\u306e\uff12
  Church-Rosser\u306e\u5b9a\u7406\u3092\u78ba\u8a8d\u3059\u308b\u4f8b
  \u6700\u5de6\u7c21\u7d04\u306e\u30b9\u30c6\u30c3\u30d7\u5b9f\u884c
  \u4ee3\u5165\u64cd\u4f5c -- M[x:=N] \u307e\u305f\u306f [N/x]M
  \u30e9\u30e0\u30c0\u5f0f\u306e\u81ea\u7531\u5909\u6570\u51fa\u529b
  \u8ad6\u7406\u6f14\u7b97
  \u6574\u6570\u306e\u52a0\u7b97
  \u518d\u5e30
  pair -- car, cdr, cons
  \u90e8\u5206\u9069\u7528
  \u95a2\u6570\u5408\u6210
  \u30de\u30af\u30ed\u5b9a\u7fa9
  \u8a08\u7b97\u7d50\u679c\u306e\u8868\u73fe\u3092\u5909\u66f4
  \u30c8\u30ec\u30fc\u30b9


\u25a0\u7c21\u7d04\u624b\u9806\u306b\u3088\u308a\u505c\u6b62\u3057\u306a\u3044\u4f8b
lambda> (\x.y)((\x.xx)(\x.xx)) ->
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 1                        [1] \u306f\u3059\u3067\u306b\u6b63\u898f\u5f62
lambda> (\x.y)((\x.xx)(\x.xx)) ->
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 2                        [2] \u3092\u9078\u3076\u3068\u505c\u6b62\u3057\u306a\u3044
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 2
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 2
    [1] y
    [2] (\x.y)((\x.xx)\x.xx)
    number or quit? 1

\u25a0\u505c\u6b62\u3057\u306a\u3044\u4f8b \u305d\u306e\uff11
lambda> (\x.xx)(\x.xx) ->
    [1] (\x.xx)\x.xx                     \u7c21\u7d04\u7d50\u679c\u304c\u5909\u5316\u3057\u306a\u3044\u305f\u3081\u505c\u6b62\u3057\u306a\u3044
    number or quit?
    [1] (\x.xx)\x.xx
    number or quit?
    [1] (\x.xx)\x.xx
    number or quit? q

\u25a0\u505c\u6b62\u3057\u306a\u3044\u4f8b \u305d\u306e\uff12
lambda> (\x.xxx)(\x.xxx) ->
    [1] ((\x.xxx)\x.xxx)\x.xxx           \u7c21\u7d04\u7d50\u679c\u304c\u3088\u308a\u8907\u96d1\u306b\u306a\u308b
    number or quit?
    [1] (((\x.xxx)\x.xxx)\x.xxx)\x.xxx
    number or quit?
    [1] ((((\x.xxx)\x.xxx)\x.xxx)\x.xxx)\x.xxx
    number or quit?
    [1] (((((\x.xxx)\x.xxx)\x.xxx)\x.xxx)\x.xxx)\x.xxx
    number or quit? q

\u25a0Church-Rosser\u306e\u5b9a\u7406\u3092\u78ba\u8a8d\u3059\u308b\u4f8b
lambda> (\y.y((\a.xa)(\a.a)))(\b.b) ->        [2],[1] \u3092\u9078\u3076\u5834\u5408
    [1] (\b.b)((\a.xa)\a.a)
    [2] (\y.y(x\a.a))\b.b
    number or quit? 2
    [1] (\b.b)(x\a.a)
    number or quit? 1
    [1] x\a.a
    number or quit?
lambda> (\y.y((\a.xa)(\a.a)))(\b.b) ->        [1],[2] \u3092\u9078\u3076\u5834\u5408
    [1] (\b.b)((\a.xa)\a.a)
    [2] (\y.y(x\a.a))\b.b
    number or quit? 1
    [1] (\a.xa)\a.a
    [2] (\b.b)(x\a.a)
    number or quit? 2
    [1] x\a.a
    number or quit?
lambda> (\y.y((\a.xa)(\a.a)))(\b.b) ->        [1],[1] \u3092\u9078\u3076\u5834\u5408
    [1] (\b.b)((\a.xa)\a.a)
    [2] (\y.y(x\a.a))\b.b
    number or quit? 1
    [1] (\a.xa)\a.a
    [2] (\b.b)(x\a.a)
    number or quit? 1
    [1] x\a.a
    number or quit?

\u25a0\u6700\u5de6\u7c21\u7d04\u306e\u30b9\u30c6\u30c3\u30d7\u5b9f\u884c
  \u8a08\u7b97\u958b\u59cb\u8a18\u53f7 => \u3092\u6307\u5b9a\u3059\u308b\u3068\u6700\u5de6\u7c21\u7d04\u306e\u307f\u306e\u30b9\u30c6\u30c3\u30d7\u5b9f\u884c\u3068\u306a\u308b.
  \u540c\u69d8\u306e\u8a18\u53f7 -> \u306f\u53ef\u80fd\u306a\u3059\u3079\u3066\u306e\uff11\u30b9\u30c6\u30c3\u30d7\u7c21\u7d04\u7d50\u679c\u3092\u51fa\u529b\u3059\u308b\u305f\u3081\u8907\u6570\u500b
  \u306e\u7d50\u679c\u304c\u51fa\u529b\u3055\u308c\u308b\u3053\u3068\u306b\u6ce8\u610f.
  \u306a\u304a\u6700\u521d\u306b\u5bfe\u8a71\u7684\u306b\u9032\u3081\u308b\u304b\u3069\u3046\u304b\u3092\u554f\u3044\u5408\u308f\u305b\u308b\u306e\u3067 s \u307e\u305f\u306f c \u3067\u5fdc\u7b54
  \u3059\u308b\u3053\u3068. \u6539\u884c\u306e\u307f\u306a\u3089\u3070 s \u3068\u307f\u306a\u3055\u308c\u308b.

lambda> (\xsz.s(xs(s(xsz))))(\sz.s(sz)) =>
stepwise or continuously? s                s \u307e\u305f\u306f\u7a7a\u884c\u3067\u30b9\u30c6\u30c3\u30d7\u5b9f\u884c\u3068\u306a\u308b
    \sz.s((\sz.s(sz))s(s((\sz.s(sz))sz)))
    ENTER or quit?
    \sz.s((\z.s(sz))(s((\sz.s(sz))sz)))
    ENTER or quit?
    \sz.s(s(s(s((\sz.s(sz))sz))))
    ENTER or quit?
    \sz.s(s(s(s((\z.s(sz))z))))
    ENTER or quit?
    \sz.s(s(s(s(s(sz)))))
    ENTER or quit?

lambda> (\xsz.s(xs(s(xsz))))(\sz.s(sz)) =>
stepwise or continuously? c                c \u306e\u5834\u5408\u306f\u5bfe\u8a71\u305b\u305a\u8a08\u7b97\u904e\u7a0b\u3092\u51fa\u529b
-> \sz.s((\sz.s(sz))s(s((\sz.s(sz))sz)))
-> \sz.s((\z.s(sz))(s((\sz.s(sz))sz)))
-> \sz.s(s(s(s((\sz.s(sz))sz))))
-> \sz.s(s(s(s((\z.s(sz))z))))
-> \sz.s(s(s(s(s(sz)))))

\u25a0\u4ee3\u5165\u64cd\u4f5c -- M[x:=N] \u307e\u305f\u306f [N/x]M
  \u03b2\u5909\u63db\u306e\u90e8\u5206\u6a5f\u80fd\u306e\u4ee3\u5165\u64cd\u4f5c\u3082\u53ef\u80fd\u3067\u3042\u308b.
  M[x:=N] \u307e\u305f\u306f [N/x]M \u306e\u5f62\u5f0f\u3067\u6307\u5b9a\u3059\u308b\u3053\u3068. [ ] := / \u306a\u3069\u306e\u8a18\u53f7\u306f\u30e9\u30e0\u30c0\u5f0f
  \u3067\u306f\u4f7f\u308f\u308c\u306a\u3044\u305f\u3081\u533a\u5225\u3067\u304d\u308b.

lambda> \sz.s(nsz)[n:=\xy.x(xy)];
\sz.s((\xy.x(xy))sz)

lambda> [\xy.x(xy)/n]\sz.s(nsz);
\sz.s((\xy.x(xy))sz)

lambda> \sz.s(nsz)[n:=<2>];
\sz.s(<2>sz)

\u25a0\u30e9\u30e0\u30c0\u5f0f\u306e\u81ea\u7531\u5909\u6570\u51fa\u529b
  \u30e9\u30e0\u30c0\u5f0f\u306e\u81ea\u7531\u5909\u6570\u3092\u898b\u3064\u3051\u308b\u6a5f\u80fd\u306f :print FV(\u30e9\u30e0\u30c0\u5f0f) \u3067\u3042\u308b.

lambda> :p FV(\xy.mx(ny))         :p \u306f :print \u306e\u7701\u7565\u5f62
{m, n}

\u25a0\u8ad6\u7406\u6f14\u7b97
  \u5b9a\u7fa9\u6e08\u307f\u306e\u30de\u30af\u30ed\u3092\u8868\u793a\u3059\u308b\u306b\u306f :macro(\u307e\u305f\u306f:m) \u3092\u5165\u529b\u3059\u308b\u3053\u3068.

lambda> <not><false>;
<true>
3 step(s) [0.000ms]
lambda> <not><true>;
<false>
3 step(s) [0.000ms]
lambda> <and><false><false>;
<false>
4 step(s) [0.000ms]
lambda> <and><false><true>;
<false>
4 step(s) [0.018ms]
lambda> <and><true><false>;
<false>
4 step(s) [0.000ms]
lambda> <and><true><true>;
<true>
4 step(s) [0.000ms]
lambda> <or><false><false>;
<false>
4 step(s) [0.000ms]
lambda> <or><false><true>;
<true>
4 step(s) [0.000ms]
lambda> <or><true><false>;
<true>
4 step(s) [0.001ms]
lambda> <or><true><true>;
<true>
4 step(s) [0.002ms]

\u25a0\u6574\u6570\u306e\u52a0\u7b97
  \u5b9a\u7fa9\u6e08\u307f\u306e\u30de\u30af\u30ed\u3092\u8868\u793a\u3059\u308b\u306b\u306f :macro(\u307e\u305f\u306f:m) \u3092\u5165\u529b\u3059\u308b\u3053\u3068.

lambda> <add><3><2> ;
<5>                          3 + 2 = 5
6 step(s) [0.000ms]
lambda> <add><3><2> ->
    [1] (\nsz.<3>s(nsz))<2>
    number or quit?
    [1] \sz.<3>s(<2>sz)
    [2] (\nsz.(\z.s(s(sz)))(nsz))<2>
    number or quit?
    [1] \sz.(\z.s(s(sz)))(<2>sz)
    [2] \sz.<3>s((\z.s(sz))z)
    number or quit?
    [1] \sz.s(s(s(<2>sz)))
    [2] \sz.(\z.s(s(sz)))((\z.s(sz))z)
    number or quit?
    [1] \sz.s(s(s((\z.s(sz))z)))
    number or quit?
    [1] <5>
    number or quit?

\u25a0\u518d\u5e30
  \u5b9a\u7fa9\u6e08\u307f\u306e\u30de\u30af\u30ed\u3092\u8868\u793a\u3059\u308b\u306b\u306f :macro(\u307e\u305f\u306f:m) \u3092\u5165\u529b\u3059\u308b\u3053\u3068.

lambda> <Y><fact><3>;          Curry\u306e\u4e0d\u52d5\u70b9\u6f14\u7b97\u5b50\u3092\u4f7f\u3063\u305f\u968e\u4e57
<6>
694 step(s) [0.858ms]
lambda> <Yt><fact><3>;         Turing\u306e\u4e0d\u52d5\u70b9\u6f14\u7b97\u5b50\u3092\u4f7f\u3063\u305f\u968e\u4e57
<6>
709 step(s) [0.400ms]

\u25a0pair -- car, cdr, cons
  \u5b9a\u7fa9\u6e08\u307f\u306e\u30de\u30af\u30ed\u3092\u8868\u793a\u3059\u308b\u306b\u306f :macro(\u307e\u305f\u306f:m) \u3092\u5165\u529b\u3059\u308b\u3053\u3068.

lambda> <car>(<cons>XY);
X
6 step(s) [0.000ms]
lambda> <cdr>(<cons>XY);
Y
6 step(s) [0.003ms]

\u25a0\u90e8\u5206\u9069\u7528
  \u4f8b\u3068\u3057\u3066
      (\mn.m+n)3 -> \n.3+n
  \u3092\u793a\u3059. \u305f\u3060\u3057 + \u3084 3 \u306a\u3069\u7565\u8a18\u6cd5\u3092\u4f7f\u3063\u3066\u3044\u308b\u3053\u3068\u306b\u6ce8\u610f.
  \u610f\u5473\u306f
      \uff12\u5909\u6570\u95a2\u6570 \mn.m+n \u3092\u5f15\u6570\uff13\u306b\u90e8\u5206\u9069\u7528\u3059\u308b\u3068\uff11\u5909\u6570\u95a2\u6570 \n.3+n \u306b\u306a\u308b
  \u3068\u3044\u3046\u3053\u3068.

lambda> (\mnsz.ms(nsz))<3>;         \u7565\u8a18\u6cd5 (\mn.m+n)3
\nsz.s(s(s(nsz)))                   \u7565\u8a18\u6cd5 \n.3+n
3 step(s) [0.002ms]

  \u5b9f\u969b\u306b\u3053\u308c\u304c\u5f15\u6570\u306b\uff13\u3092\u52a0\u7b97\u3059\u308b\u95a2\u6570\u3068\u306a\u3063\u3066\u3044\u308b\u3053\u3068\u3092\u78ba\u8a8d\u3059\u308b\u305f\u3081\u306b
      (\n.3+n)2 -> 5
  \u3068\u306a\u308b\u3053\u3068\u3092\u793a\u3059.

lambda> (\nsz.s(s(s(nsz))))<2>;        \u7565\u8a18\u6cd5 (\n.3+n)2
<5>                                    \u7565\u8a18\u6cd5 5
3 step(s) [0.001ms]

\u25a0\u95a2\u6570\u5408\u6210
  \u95a2\u6570 f \u3068 g \u306e\u95a2\u6570\u5408\u6210\u306f \fgx.g(fx) \u3067\u8868\u73fe\u3067\u304d\u308b.
  \u5177\u4f53\u7684\u306a\uff12\u3064\u306e\u95a2\u6570
      add1 = <add><1> = (\mnsz.ms(nsz))(\sz.sz)    \u7565\u8a18\u6cd5 \x.1+x
      mul2 = <mul><2> = (\mns.m(ns))(\sz.s(sz))      \u7565\u8a18\u6cd5 \x.2*x
  \u306e\u95a2\u6570\u5408\u6210\u306f
      (\fgx.g(fx))<add1><mul2>                      \u7565\u8a18\u6cd5 \x.2*(1+x)
  \u3068\u306a\u308b.

lambda> (\fgx.g(fx))((\mnsz.ms(nsz))<1>)((\mns.m(ns))<2>);
\xsz.s(xs(s(xsz)))
17 step(s) [0.002ms]

  \u5b9f\u969b\u306b\u3053\u308c\u304c\u524d\u8ff0\u306e\u5408\u6210\u95a2\u6570\u3068\u306a\u3063\u3066\u3044\u308b\u3053\u3068\u3092\u78ba\u8a8d\u3059\u308b\u305f\u3081\u306b
      (\x.2*(1+x))5 -> 12
  \u3068\u306a\u308b\u3053\u3068\u3092\u793a\u3059.

lambda> (\xsz.s(xs(s(xsz))))<5>;    \u7565\u8a18\u6cd5 (\x.2*(1+x))5
<12>                                \u7565\u8a18\u6cd5 12
5 step(s) [0.001ms]

\u25a0\u30de\u30af\u30ed\u5b9a\u7fa9
  \u30de\u30af\u30ed\u5b9a\u7fa9\u306e\u30b7\u30f3\u30bf\u30af\u30b9\u306f
      \u30de\u30af\u30ed\u540d = \u30e9\u30e0\u30c0\u5f0f ;
  \u3067\u3042\u308b.
  \u30d5\u30a1\u30a4\u30eb\u306b\u30de\u30af\u30ed\u5b9a\u7fa9\u3092\u8a18\u8ff0\u3057\u3066\u3042\u308b\u5834\u5408\u306f\u4e0b\u8a18\u306e\u65b9\u6cd5\u3067\u30ed\u30fc\u30c9\u3067\u304d\u308b.
    (1) :load \u30b3\u30de\u30f3\u30c9\u3067\u5b9f\u884c\u4e2d\u306b\u8aad\u307f\u8fbc\u3080.
    (2) \u30b3\u30de\u30f3\u30c9\u884c\u5f15\u6570 -l \u30aa\u30d7\u30b7\u30e7\u30f3\u3067\u8d77\u52d5\u6642\u306b\u8aad\u307f\u8fbc\u3080.

lambda> add1mul = \xsz.s(xs(s(xsz)));       \u7565\u8a18\u6cd5 \x.2*(1+x)
lambda> <add1mul><3>;
<8>                                         \u7565\u8a18\u6cd5 8
5 step(s) [0.000ms]

lambda> :load macrofile     \u30d5\u30a1\u30a4\u30eb\u304b\u3089\u30de\u30af\u30ed\u5b9a\u7fa9\u3092\u8aad\u307f\u8fbc\u3080.

\u25a0\u8a08\u7b97\u7d50\u679c\u306e\u8868\u73fe\u3092\u5909\u66f4
  \u7d50\u679c\u3092\u51fa\u529b\u3059\u308b\u969b\u306b :format \u30b3\u30de\u30f3\u30c9\u3067\u8868\u73fe\u3092\u5909\u66f4\u3067\u304d\u308b.
  :format \u30b3\u30de\u30f3\u30c9\u306e\u5f15\u6570\u3068\u3057\u3066\u53ef\u80fd\u306a\u5024\u306f\u6b21\u306e\u3068\u304a\u308a.
         abbrev \u6700\u3082\u7c21\u6f54\u306a\u6570\u5b66\u7684\u8868\u73fe   [\u4f8b] \u03bbxy.xyz
         math   \u7c21\u6f54\u306a\u901a\u5e38\u306e\u6570\u5b66\u7684\u8868\u73fe [\u4f8b] \u03bbx.\u03bby.xyz
         proper \u62ec\u5f27\u306e\u591a\u3044\u6570\u5b66\u7684\u8868\u73fe   [\u4f8b] \u03bbx.(\u03bby.((xy)z))
  \u3055\u3089\u306b :reshape \u30b3\u30de\u30f3\u30c9\u3067\u7d50\u679c\u306e\u6587\u5b57\u5217\u3092\u30de\u30af\u30ed\u540d\u306b\u7f6e\u304d\u63db\u3048\u308b\u304b\u3069\u3046\u304b\u3092
  \u5236\u5fa1\u3067\u304d\u308b. \u30c7\u30d5\u30a9\u30eb\u30c8\u52d5\u4f5c\u306f\u30de\u30af\u30ed\u540d\u306b\u7f6e\u304d\u63db\u3048\u308b.

lambda> :format proper
lambda> \xy.xyz;
\x.(\y.((xy)z))           \u62ec\u5f27\u304c\u591a\u3044\u305f\u3081\u30e9\u30e0\u30c0\u5f0f\u306e\u69cb\u9020\u304c\u660e\u78ba\u306b\u306a\u308b.
0 step(s) [0.001ms]
lambda> :f math
lambda> \xy.xyz;
\x.\y.xyz                 \u30e9\u30e0\u30c0\u62bd\u8c61\u304c\uff11\u5f15\u6570\u3067\u8868\u73fe\u3055\u308c\u308b.
0 step(s) [0.000ms]
lambda> :f abbrev
lambda> \xy.xyz;
\xy.xyz                   \u901a\u5e38\u306f\u3053\u306e\u5f62\u5f0f\u3067\u51fa\u529b\u3055\u308c\u308b.
0 step(s) [0.000ms]

lambda> :reshape off      \u30de\u30af\u30ed\u540d\u306b\u7f6e\u304d\u63db\u3048\u306a\u3044\u8a2d\u5b9a
lambda> <Y><fact><3>;
\sz.s(s(s(s(s(sz)))))     \u3053\u308c\u306f <6> \u3092\u610f\u5473\u3059\u308b.
694 step(s) [0.762ms]
lambda> :r                \u30de\u30af\u30ed\u540d\u306b\u7f6e\u304d\u63db\u3048\u308b\u8a2d\u5b9a
lambda> <Y><fact><3>;
<6>                       \u7d50\u679c\u3092\u5b9a\u7fa9\u6e08\u307f\u30de\u30af\u30ed\u306b\u7f6e\u304d\u63db\u3048\u3066\u3044\u308b.
694 step(s) [0.761ms]

\u25a0\u30c8\u30ec\u30fc\u30b9
  :trace \u30b3\u30de\u30f3\u30c9\u3067\u30c8\u30ec\u30fc\u30b9\u51fa\u529b\u3092\u5236\u5fa1\u3067\u304d\u308b.
  \u30c8\u30ec\u30fc\u30b9\u51fa\u529b\u306e\u8aac\u660e
    \u30fb->\u8a18\u53f7\u306f\u7c21\u7d04\u7d50\u679c\u3092\u8868\u3059.
    \u30fb\u30a4\u30f3\u30c7\u30f3\u30c8\u306f\u90e8\u5206\u5f0f\u306e\u8a08\u7b97\u3067\u3042\u308b\u3053\u3068\u3092\u8868\u3059.
    \u30fb--\u8a18\u53f7\u306f\u8a72\u5f53\u3057\u305f\u03b2\u5909\u63db\u306e\u898f\u5247\u3092\u8868\u3059. (\u8a08\u7b97\u8ad6 \u9ad8\u6a4b\u6b63\u5b50\u8457 p.65)

lambda> :t              \u30c8\u30ec\u30fc\u30b9\u51fa\u529b\u958b\u59cb
lambda> <succ><3>;
<succ><3>
  \sz.s(nsz)[n:=<3>]  -- (\u03bbx.M)N\u2192M[x:=N]
-> \sz.s(<3>sz)
\sz.s(<3>sz)
  \z.s(<3>sz)  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
    s(<3>sz)  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
      <3>sz  -- PM\u2192PN if M\u2192N
        <3>s  -- MP\u2192NP if M\u2192N
          \z.s(s(sz))[s:=s]  -- (\u03bbx.M)N\u2192M[x:=N]
        -> \z.s(s(sz))  -- MP\u2192NP if M\u2192N
      -> (\z.s(s(sz)))z  -- PM\u2192PN if M\u2192N
    -> s((\z.s(s(sz)))z)  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
  -> \z.s((\z.s(s(sz)))z)  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
-> \sz.s((\z.s(s(sz)))z)
\sz.s((\z.s(s(sz)))z)
  \z.s((\z.s(s(sz)))z)  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
    s((\z.s(s(sz)))z)  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
      (\z.s(s(sz)))z  -- PM\u2192PN if M\u2192N
        s(s(sz))[z:=z]  -- (\u03bbx.M)N\u2192M[x:=N]
      -> s(s(sz))  -- PM\u2192PN if M\u2192N
    -> s(s(s(sz)))  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
  -> \z.s(s(s(sz)))  -- \u03bbx.M\u2192\u03bbx.N if M\u2192N
-> <4>
<4>
3 step(s) [0.008ms]

lambda> :t off          \u30c8\u30ec\u30fc\u30b9\u51fa\u529b\u505c\u6b62
lambda> <succ><3>;
<4>
3 step(s) [0.000ms]

