Hot
Jump to navigation
Jump to search
| Paradigm(s) | Functional |
|---|---|
| Designed by | User:Hakerh400 |
| Appeared in | 2021 |
| Computational class | Turing complete |
| Reference implementation | Unimplemented |
| File extension(s) | .txt |
Hot is a computational model inspired by Zot. Hot is a pure functional language. All functions are side-effect-free, including I/O operations (from the perspective of the program itself, of course). The main difference between Zot and Hot is that the I/O actions in Hot are much simpler and more concise that the I/O actions in Zot.
Overview
Hot has the following combinators:
K, S, F, A, B, C, D, 0, 1
And the following rewriting rules:
K x y ---> x S x y z ---> x z (y z) F x ---> x B A A x ---> x # // # is the next input bit B x ---> x D C C x ---> x // and output bit 0 D x ---> x // and output bit 1 0 x y ---> y 1 ---> K
Unlike in other calculi (such as SKI, Jot, Iota, Zot, etc), rewriting rules in Hot can be applied only at the beginning of the main expression. For example, in the following expression:
0 (C K) (D K)
we cannot reduce (C K) or (D K), because they are not at the beginning of the main expression. We can only reduce 0, so the expression becomes:
D K
and now we can reduce it to K and output bit 1.
Also, another difference between SKI and Hot is that a program in Hot does not halt on its own. Instead, if there are not enough arguments to perform the leftmost reduction, we append required number of F combinators. For example, if the source code consists only of combinator K, we clearly cannot apply any reduction. So, we append two F combinators, because K takes two arguments:
K F F
Then we reduce it to
F
Now, F takes one argument, so we append another F and the main expression becomes:
F F
Then we keep reducing it (assuming all input bits are 0):
F B A B B A A B D C A A D D C C A A D C C A A // out 1 C C A A // out 1 C A A // out 0 A A // out 0 A 0 0 0 0 0 F F F F ...
I/O format
Input is a binary string. Each bit of the string is prepended with 1 and then infinitely many 0s are appended. Similarly, when the program outputs 0 on an even position (0-indexed), then the program halts and the output is the sequence of bits at odd positions.
For example, if we feed input string 1011 to a Hot program, it will be transformed into
1110111100000000000000000000...
And suppose the program produces string
1010110|1010001010110101...
The | represents the point at which the program halts (because 0 appeared on an even position) and the rest of bits are ignored. The output is 001.
Examples
Truth machine
Code:
S(S(K(S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))))))(S(SKK)(K(SK))))(S(SKK)(KK))
Step-by-step computation for the case when the input is 0:
S(S(K(S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))))))(S(SKK)(K(SK))))(S(SKK)(KK)) S(K(S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))))))(S(SKK)(K(SK)))F(S(SKK)(KK)F) K(S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))))F(S(SKK)(K(SK))F)(S(SKK)(KK)F) S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))))(S(SKK)(K(SK))F)(S(SKK)(KK)F) K(S(S(SKK)(KK)))(S(SKK)(K(SK))F)(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) S(S(SKK)(KK))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) S(SKK)(KK)(S(SKK)(KK)F)(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKK(S(SKK)(KK)F)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) K(S(SKK)(KK)F)(K(S(SKK)(KK)F))(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) S(SKK)(KK)F(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKKF(KKF)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KF(KF)(KKF)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) F(KKF)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KKFBA(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KBA(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) B(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KK(S(SKK)(KK)F)DC(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KDC(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) D(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) ---> OUT 1 S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F) S(KS)K(S(SKK)(K(SK))F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) KS(S(SKK)(K(SK))F)(K(S(SKK)(K(SK))F))(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) S(K(S(SKK)(K(SK))F))(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) K(S(SKK)(K(SK))F)(S(SKK)(KK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) S(SKK)(K(SK))F(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKKF(K(SK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KF(KF)(K(SK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) F(K(SK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) K(SK)FBA(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKBA(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KA(BA)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) A(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) ---> IN 1 S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)1 S(KS)K(S(SKK)(K(SK))F)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F))(S(SKK)(KK)F)1 KS(S(SKK)(K(SK))F)(K(S(SKK)(K(SK))F))(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F))(S(SKK)(KK)F)1 S(K(S(SKK)(K(SK))F))(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F))(S(SKK)(KK)F)1 K(S(SKK)(K(SK))F)(S(SKK)(KK)F)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F))1 S(SKK)(K(SK))F(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F))1 A(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F))1 ---> IN 0 K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F)01 S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))(S(SKK)(KK)F)01 S(K(SS))(S(SKK)(SKK))(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)01 K(SS)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)01 SS(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)01 S(S(SKK)(KK)F)(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F))01 S(SKK)(KK)F0(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)0)1 B0(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)0)1 0DC(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)0)1 C(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)0)1 ---> OUT 0 S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)01 SKK(S(K(SS))(S(SKK)(SKK)))(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)01 K(S(K(SS))(S(SKK)(SKK)))(K(S(K(SS))(S(SKK)(SKK))))(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)01 S(K(SS))(S(SKK)(SKK))(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)01 K(SS)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)01 SS(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)01 S(S(SKK)(KK)F)(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F))01 S(SKK)(KK)F0(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)0)1 B0(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)0)1 0DC(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)0)1 C(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)0)1 ---> OUT 0 ---> HALT
Explanation: when the input is 0, it means that the program sees the following sequence of bits in the input (see the I/O format section for details):
100000000000...
The program then outputs:
100
the second 0 appears on an even position, so the program halts and the actual output is 0.
Here is the step-by-step computation for the case when the input is 1:
S(S(K(S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))))))(S(SKK)(K(SK))))(S(SKK)(KK)) S(K(S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))))))(S(SKK)(K(SK)))F(S(SKK)(KK)F) K(S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))))F(S(SKK)(K(SK))F)(S(SKK)(KK)F) S(K(S(S(SKK)(KK))))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))))(S(SKK)(K(SK))F)(S(SKK)(KK)F) K(S(S(SKK)(KK)))(S(SKK)(K(SK))F)(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) S(S(SKK)(KK))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) S(SKK)(KK)(S(SKK)(KK)F)(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKK(S(SKK)(KK)F)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) K(S(SKK)(KK)F)(K(S(SKK)(KK)F))(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) S(SKK)(KK)F(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKKF(KKF)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KF(KF)(KKF)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) F(KKF)(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KKFBA(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KBA(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) B(KK(S(SKK)(KK)F))(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KK(S(SKK)(KK)F)DC(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KDC(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) D(S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) ---> OUT 1 S(S(KS)K)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))))(S(SKK)(K(SK))F)(S(SKK)(KK)F) S(KS)K(S(SKK)(K(SK))F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) KS(S(SKK)(K(SK))F)(K(S(SKK)(K(SK))F))(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) S(K(S(SKK)(K(SK))F))(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F))(S(SKK)(KK)F) K(S(SKK)(K(SK))F)(S(SKK)(KK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) S(SKK)(K(SK))F(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKKF(K(SK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KF(KF)(K(SK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) F(K(SK)F)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) K(SK)FBA(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) SKBA(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) KA(BA)(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) A(S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)) ---> IN 1 S(S(KS)K)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))))(S(SKK)(K(SK))F)(S(SKK)(KK)F)1 S(KS)K(S(SKK)(K(SK))F)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F))(S(SKK)(KK)F)1 KS(S(SKK)(K(SK))F)(K(S(SKK)(K(SK))F))(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F))(S(SKK)(KK)F)1 S(K(S(SKK)(K(SK))F))(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F))(S(SKK)(KK)F)1 K(S(SKK)(K(SK))F)(S(SKK)(KK)F)(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F))1 S(SKK)(K(SK))F(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F))1 A(K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F))1 ---> IN 1 K(S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK)))(S(SKK)(K(SK))F)(S(SKK)(KK)F)11 S(S(K(SS)))(S(K(SS)))(S(SKK)(SKK))(S(SKK)(KK)F)11 S(K(SS))(S(SKK)(SKK))(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)11 K(SS)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)11 SS(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)11 S(S(SKK)(KK)F)(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F))11 S(SKK)(KK)F1(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)1)1 B1(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)1)1 1DC(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)1)1 KDC(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)1)1 D(S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)1)1 ---> OUT 1 S(SKK)(SKK)(S(K(SS))(S(SKK)(SKK)))(S(SKK)(KK)F)11 SKK(S(K(SS))(S(SKK)(SKK)))(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)11 K(S(K(SS))(S(SKK)(SKK)))(K(S(K(SS))(S(SKK)(SKK))))(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)11 S(K(SS))(S(SKK)(SKK))(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)11 K(SS)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 SS(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 S(S(SKK)(KK)F)(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F))11 S(SKK)(KK)F1(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)1)1 B1(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)1)1 1DC(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)1)1 KDC(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)1)1 D(S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)1)1 ---> OUT 1 S(SKK)(SKK)(SKK(S(K(SS))(S(SKK)(SKK))))(S(SKK)(KK)F)11 SKK(SKK(S(K(SS))(S(SKK)(SKK))))(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 K(SKK(S(K(SS))(S(SKK)(SKK))))(K(SKK(S(K(SS))(S(SKK)(SKK)))))(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 SKK(S(K(SS))(S(SKK)(SKK)))(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 K(S(K(SS))(S(SKK)(SKK)))(K(S(K(SS))(S(SKK)(SKK))))(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 S(K(SS))(S(SKK)(SKK))(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 K(SS)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK))))))(S(SKK)(KK)F)11 SS(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK))))))(S(SKK)(KK)F)11 S(S(SKK)(KK)F)(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F))11 S(SKK)(KK)F1(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)1)1 B1(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)1)1 1DC(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)1)1 KDC(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)1)1 D(S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)1)1 ---> OUT 1 S(SKK)(SKK)(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(S(SKK)(KK)F)11 SKK(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(SKK(SKK(SKK(S(K(SS))(S(SKK)(SKK))))))(S(SKK)(KK)F)11 K(SKK(SKK(S(K(SS))(S(SKK)(SKK)))))(K(SKK(SKK(S(K(SS))(S(SKK)(SKK))))))(SKK(SKK(SKK(S(K(SS))(S(SKK)(SKK))))))(S(SKK)(KK)F)11 SKK(SKK(S(K(SS))(S(SKK)(SKK))))(SKK(SKK(SKK(S(K(SS))(S(SKK)(SKK))))))(S(SKK)(KK)F)11 K(SKK(S(K(SS))(S(SKK)(SKK))))(K(SKK(S(K(SS))(S(SKK)(SKK)))))(SKK(SKK(SKK(S(K(SS))(S(SKK)(SKK))))))(S(SKK)(KK)F)11 ...