[| x |] = λk.k x ・・・val
[| λx.t |] = λk.k (λx.[|t|]) ・・・lam
[| π t |] = λk.[|t|] (λa.k (π a)) ・・・app1
[| t1 t2 |] = λk.[|t1|] (λf.[|t2|] (λa.f a k)) ・・・app2
[| π t1 t2 |] = λk.[|t1|] (λa.[|t2|] (λb.k (π a b)))・・・app3
[| Sx.t |] = λk.[x↦λa.λk'.k' (k a)]([|t|] (λv.v))・・・shift
[| <t> |] = λk.k ([|t|] (λv.v)) ・・・reset
[|<concat (Sk.λx.k x) (Sk.λx.k (i2s x))> "a" 10|]
1. app2 -> λk1.[|<concat (Sk.λx.k x) (Sk.λx.k (i2s x))> "a"|] (λf1.[|10|] (λa1.f1 a1 k1))
2. app2 -> λk1.(λk2.[|<concat (Sk.λx.k x) (Sk.λx.k (i2s x))>|] (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
3. reset -> λk1.(λk2.(λk3.k3 ([|concat (Sk.λx.k x) (Sk.λx.k (i2s x))|] id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
4. app3 -> λk1.(λk2.(λk3.k3 ((λk4.[|Sk.λx.k x|] (λa4.[|Sk.λx.k (i2s x)|] (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
5. shift -> λk1.(λk2.(λk3.k3 ((λk4.(λk5.[k↦(λa5.λk'.k' (k5 a5))]{[|λx.k x|] id-shift}) (λa4.[|Sk.λx.k (i2s x)|] (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
6. lam -> λk1.(λk2.(λk3.k3 ((λk4.(λk5.[k↦(λa5.λk'.k' (k5 a5))]{(λk6.k6 (λx.[|k x|] )) id-shift}) (λa4.[|Sk.λx.k (i2s x)|] (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
7. app2 -> λk1.(λk2.(λk3.k3 ((λk4.(λk5.[k↦(λa5.λk'.k' (k5 a5))]{(λk6.k6 (λx.(λk7.[|k|] (λf7.[|x|] (λa7.f7 a7 k7))))) id-shift}) (λa4.[|Sk.λx.k (i2s x)|] (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
8. val -> λk1.(λk2.(λk3.k3 ((λk4.(λk5.[k↦(λa5.λk'.k' (k5 a5))]{(λk6.k6 (λx.(λk7.(λk8.k8 k ) (λf7.[|x|] (λa7.f7 a7 k7))))) id-shift}) (λa4.[|Sk.λx.k (i2s x)|] (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
9. val -> λk1.(λk2.(λk3.k3 ((λk4.(λk5.[k↦(λa5.λk'.k' (k5 a5))]{(λk6.k6 (λx.(λk7.(λk8.k8 k ) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift}) (λa4.[|Sk.λx.k (i2s x)|] (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
= λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.[|Sk.λx.k (i2s x)|] (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
10.shift -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10.[k↦(λa10.λk'.k' (k10 a10))]([|λx.k (i2s x)|] id-shift)) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
11.lam -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10.[k↦(λa10.λk'.k' (k10 a10))]((λk11.k11 (λx.[|k (i2s x)|] )) id-shift)) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
12.app2 -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10.[k↦(λa10.λk'.k' (k10 a10))]((λk11.k11 (λx.(λk12.[|k|] (λf12.[|i2s x|] (λa12.f12 a12 k12))))) id-shift)) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
13.val -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10.[k↦(λa10.λk'.k' (k10 a10))]((λk11.k11 (λx.(λk12.(λk13.k13 k ) (λf12.[|i2s x|] (λa12.f12 a12 k12))))) id-shift)) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
14.app1 -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10.[k↦(λa10.λk'.k' (k10 a10))]((λk11.k11 (λx.(λk12.(λk13.k13 k ) (λf12.(λk14.[|x|] (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift)) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
15.val -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10.[k↦(λa10.λk'.k' (k10 a10))]((λk11.k11 (λx.(λk12.(λk13.k13 k ) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift)) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
= λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.[|"a"|] (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
16.val -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.(λk16.k16 "a") (λa2.f2 a2 k2))) (λf1.[|10|] (λa1.f1 a1 k1))
17.val -> λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.(λk16.k16 "a") (λa2.f2 a2 k2))) (λf1.(λk17.k17 10) (λa1.f1 a1 k1))
簡約(idはさっさとつぶす)
(λk1.(λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.(λk16.k16 "a") (λa2.f2 a2 k2))) (λf1.(λk17.k17 10) (λa1.f1 a1 k1))) id
↝ (λk2.(λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.(λk16.k16 "a") (λa2.f2 a2 k2))) (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ (λk3.k3 ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset)) (λf2.(λk16.k16 "a") (λa2.f2 a2 (λf1.(λk17.k17 10) (λa1.f1 a1 id))))
↝ (λf2.(λk16.k16 "a") (λa2.f2 a2 (λf1.(λk17.k17 10) (λa1.f1 a1 id)))) ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset)
↝ (λk16.k16 "a") (λa2.((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset) a2 (λf1.(λk17.k17 10) (λa1.f1 a1 id)))
↝ (λa2.((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset) a2 (λf1.(λk17.k17 10) (λa1.f1 a1 id))) "a"
↝ ((λk4.(λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.k4 (concat a4 b4)))) id-reset) "a" (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ ((λk5. (λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' (k5 a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift ) (λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4)))) "a" (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ ((λk6.k6 (λx.(λk7.(λk8.k8 (λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) id-shift) "a" (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ (id-shift (λx.(λk7.(λk8.k8 (λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7))))) "a" (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ (λx.(λk7.(λk8.k8 (λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5))) (λf7.(λk9.k9 x) (λa7.f7 a7 k7)))) "a" (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ (λk7.(λk8.k8 (λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5))) (λf7.(λk9.k9 "a") (λa7.f7 a7 k7))) (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ (λk8.k8 (λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5))) (λf7.(λk9.k9 "a") (λa7.f7 a7 (λf1.(λk17.k17 10) (λa1.f1 a1 id))))
↝ (λf7.(λk9.k9 "a") (λa7.f7 a7 (λf1.(λk17.k17 10) (λa1.f1 a1 id)))) (λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5))
↝ (λk9.k9 "a") (λa7.(λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5)) a7 (λf1.(λk17.k17 10) (λa1.f1 a1 id)))
↝ (λa7.(λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5)) a7 (λf1.(λk17.k17 10) (λa1.f1 a1 id))) "a"
↝ (λa5.λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) a5)) "a" (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ (λk'.k' ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) "a")) (λf1.(λk17.k17 10) (λa1.f1 a1 id))
↝ (λf1.(λk17.k17 10) (λa1.f1 a1 id)) ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) "a")
↝ (λk17.k17 10) (λa1.((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) "a") a1 id)
↝ (λa1.((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) "a") a1 id) 10
↝ ((λa4.(λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat a4 b4))) "a") 10 id
↝ ((λk10. (λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' (k10 a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift ) (λb4.id-reset (concat "a" b4))) 10 id
↝ ((λk11.k11 (λx.(λk12.(λk13.k13 (λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) id-shift) 10 id
↝ (id-shift (λx.(λk12.(λk13.k13 (λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))))) 10 id
↝ (λx.(λk12.(λk13.k13 (λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10))) (λf12.(λk14.(λk15.k15 x) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12)))) 10 id
↝ (λk12.(λk13.k13 (λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10))) (λf12.(λk14.(λk15.k15 10) (λa14.k14 (i2s a14))) (λa12.f12 a12 k12))) id
↝ (λk13.k13 (λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10))) (λf12.(λk14.(λk15.k15 10) (λa14.k14 (i2s a14))) (λa12.f12 a12 id))
↝ (λf12.(λk14.(λk15.k15 10) (λa14.k14 (i2s a14))) (λa12.f12 a12 id)) (λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10))
↝ (λk14.(λk15.k15 10) (λa14.k14 (i2s a14))) (λa12.(λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10)) a12 id)
↝ (λk15.k15 10) (λa14.(λa12.(λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10)) a12 id) (i2s a14))
↝ (λa14.(λa12.(λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10)) a12 id) (i2s a14)) 10
↝ (λa12.(λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10)) a12 id) (i2s 10)
↝ (λa12.(λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10)) a12 id) "10"
↝ (λa10.λk'.k' ((λb4.id-reset (concat "a" b4)) a10)) "10" id
↝ (λk'.k' ((λb4.id-reset (concat "a" b4)) "10")) id
↝ id ((λb4.id-reset (concat "a" b4)) "10")
↝ (λb4.id-reset (concat "a" b4)) "10"
↝ id-reset (concat "a" "10")
↝ concat "a" "10"
↝ "a10"
Last active
May 7, 2019 07:01
-
-
Save bleis-tift/d4dd7ed393b8360db9a5e01604433450 to your computer and use it in GitHub Desktop.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment