1 push (\u1 -> (\u2 -> (\u3 -> (\u4 -> (\u5 -> (\u6 -> (u4 u5) u6))))))
3 | push (\u1 -> (\u2 -> u2))
6 lift (\u1 -> (\u2 -> u1 u2))
9 | | push (\u1 -> (\u2 -> u2))
13 | | push (\u1 -> (\u2 -> u2))
15 | | lift (\u1 -> (\u2 -> u1 u2))
17 | | lift (\u1 -> (\u2 -> u1 u2))
20 | lift (\u1 -> (\u2 -> u1 u2))
22 | lift (\u1 -> (\u2 -> u1 u2))
25 lift (\u1 -> (\u2 -> u1 u2))
30 lift (\u1 -> (\u2 -> u1 u2))
32 lift (\u1 -> (\u2 -> u1 u2))
36 | | push (\u1 -> (\u2 -> u2))
38 | | lift (\u1 -> (\u2 -> u1 u2))
40 | | lift (\u1 -> (\u2 -> u1 u2))
43 | lift (\u1 -> (\u2 -> u1 u2))
45 | lift (\u1 -> (\u2 -> u1 u2))
48 lift (\u1 -> (\u2 -> u1 u2))
50 lift (\u1 -> (\u2 -> u1 u2))