| axxu11(tt, X, Y, U) | ⇒ | axxu12(axxsplitAt(mark(X), mark(U)), Y)
|
| axxu12(pair(V, W), P) | ⇒ | pair(cons(mark(P), V), mark(W))
|
| axxafterNth(X1, Y1) | ⇒ | axxsnd(axxsplitAt(mark(X1), mark(Y1)))
|
| axxand(tt, U1) | ⇒ | mark(U1)
|
| axxfst(pair(V1, W1)) | ⇒ | mark(V1)
|
| axxhead(cons(P1, X2)) | ⇒ | mark(P1)
|
| axxnatsFrom(Y2) | ⇒ | cons(mark(Y2), natsFrom(s(Y2)))
|
| axxsel(U2, V2) | ⇒ | axxhead(axxafterNth(mark(U2), mark(V2)))
|
| axxsnd(pair(W2, P2)) | ⇒ | mark(P2)
|
| axxsplitAt(0, X3) | ⇒ | pair(nil, mark(X3))
|
| axxsplitAt(s(Y3), cons(U3, V3)) | ⇒ | axxu11(tt, Y3, U3, V3)
|
| axxtail(cons(W3, P3)) | ⇒ | mark(P3)
|
| axxtake(X4, Y4) | ⇒ | axxfst(axxsplitAt(mark(X4), mark(Y4)))
|
| mark(u11(U4, V4, W4, P4)) | ⇒ | axxu11(mark(U4), V4, W4, P4)
|
| mark(u12(X5, Y5)) | ⇒ | axxu12(mark(X5), Y5)
|
| mark(splitAt(U5, V5)) | ⇒ | axxsplitAt(mark(U5), mark(V5))
|
| mark(afterNth(W5, P5)) | ⇒ | axxafterNth(mark(W5), mark(P5))
|
| mark(snd(X6)) | ⇒ | axxsnd(mark(X6))
|
| mark(and(Y6, U6)) | ⇒ | axxand(mark(Y6), U6)
|
| mark(fst(V6)) | ⇒ | axxfst(mark(V6))
|
| mark(head(W6)) | ⇒ | axxhead(mark(W6))
|
| mark(natsFrom(P6)) | ⇒ | axxnatsFrom(mark(P6))
|
| mark(sel(X7, Y7)) | ⇒ | axxsel(mark(X7), mark(Y7))
|
| mark(tail(U7)) | ⇒ | axxtail(mark(U7))
|
| mark(take(V7, W7)) | ⇒ | axxtake(mark(V7), mark(W7))
|
| mark(tt) | ⇒ | tt
|
| mark(pair(P7, X8)) | ⇒ | pair(mark(P7), mark(X8))
|
| mark(cons(Y8, U8)) | ⇒ | cons(mark(Y8), U8)
|
| mark(s(V8)) | ⇒ | s(mark(V8))
|
| mark(0) | ⇒ | 0
|
| mark(nil) | ⇒ | nil
|
| axxu11(W8, P8, X9, Y9) | ⇒ | u11(W8, P8, X9, Y9)
|
| axxu12(U9, V9) | ⇒ | u12(U9, V9)
|
| axxsplitAt(W9, P9) | ⇒ | splitAt(W9, P9)
|
| axxafterNth(X10, Y10) | ⇒ | afterNth(X10, Y10)
|
| axxsnd(U10) | ⇒ | snd(U10)
|
| axxand(V10, W10) | ⇒ | and(V10, W10)
|
| axxfst(P10) | ⇒ | fst(P10)
|
| axxhead(X11) | ⇒ | head(X11)
|
| axxnatsFrom(Y11) | ⇒ | natsFrom(Y11)
|
| axxsel(U11, V11) | ⇒ | sel(U11, V11)
|
| axxtail(W11) | ⇒ | tail(W11)
|
| axxtake(P11, X12) | ⇒ | take(P11, X12)
|