*** ACK 5.65s--> Input: \f -> f 0 0 == 1 && (f 1 0 == 2) && (f 2 0 == 3) && (f 3 0 == 5) && (f 0 1 == 2) && (f 1 1 == 3) && (f 2 1 == 5) && (f 3 1 == 13) && (f 0 2 == 3) && (f 1 2 == 4) && (f 2 2 == 7) Output : (\ a b -> nat_para a (\ c -> c) (\ c d e -> nat_para e (inc zero) (\ f g -> d (inc g))) (inc b)) Output Library: TIMEOUT *** ADD 0.02s --> Input: \f -> f 0 0 == 0 && (f 1 0 == 1) && (f 2 0 == 2) && (f 3 0 == 3) && (f 0 1 == 1) && (f 1 1 == 2) && (f 2 1 == 3) && (f 3 1 == 4) && (f 0 2 == 2) && (f 1 2 == 3) && (f 2 2 == 4) Output : (\ a b -> nat_para b (\ c -> c) (\ c d e -> inc (d e)) a) *** Append 0.08s--> Input: \f -> f "" "" == "" && (f "1" "" == "1") && (f "1" "2" == "12") && (f "" "2" == "2") && (f "12" "3" == "123")&& (f "1" "23" == "123") Output : \a b -> list_para a b (\c d e -> c : e) *** CAR < 0.001s --> Input: \f -> f [] == Nothing && (f "1" == Just '1') && (f "12" == Just '1') && (f "123" == Just '1') Output : \a -> hd a *** CDR 0.004s--> Input: \f -> f "" == "" && (f "1" == "") && (f "12" == "2") && (f "123" == "23") Output : \a -> list_para a a (\b c d -> c) *** CLEARBLOCK --> Input: Output : *** DROP timeout --> Input: \f -> f 0 "" == "" && (f 1 "" == "") && (f 2 "" == "") && (f 3 "" == "") && (f 4 "" == "") && (f 0 "x" == "x") && (f 1 "x" == "") && (f 2 "x" == "") && (f 0 "x y" == "") && (f 1 "x y" == "y") && (f 2 "x y" == "") Output : TIMEOUT *** EQ 19.67s --> Input: \f -> f 0 0 == 1 && (f 0 1 == 0) && (f 1 1 == 1) && (f 1 2 == 0) && (f 2 2 == 1) && (f 3 2 == 0) && (f 3 3 == 1) Output : \ a b -> nat_para (nat_para a (\ c -> c) (\ c d e -> nat_para (d e) e (\ f g -> f)) b) (inc zero) (\ c d -> zero) *** EVEN 0.14s --> Input: \f -> f 0 == 1 && (f 1 == 0) && (f 2 == 1) && (f 3 == 0) Output : \ a -> nat_para a (inc zero) (\ b c -> nat_para c (inc zero) (\ d e -> zero)) *** EVENLIST 0.19s--> Input: \f -> f [] == 1 && (f [1] == 0) && (f [1,2] == 1) && (f [1,2,3] == 0) && (f [2,3,4,5] == 1) Output : \ a -> list_para a (inc zero) (\ b c d -> nat_para d (inc zero) (\ e f -> zero)) *** EVENPOS 4.01s --> Input: \f -> f [] == [] && (f [1] == []) && (f [1,2] == [2]) && (f [1,2,3] == [2]) && (f [1,2,3,4] == [2,4]) && (f [1,2,3,4,5] == [2,4]) && (f [1,2,3,4,5,6] == [2,4,6]) Output : (\ a -> list_para a (\ b -> nil) (\ b c d e -> nat_para e (d b) (\ f g -> cons b (d zero))) zero) *** EVENSLIST timeout--> Input: \f -> f [] == False && (f [0] == True) && (f [1] == False) && (f [2] == True) && (f [3] == False) && (f [0,0] == True) && (f [0,1] == False) && (f [0,2] == True) && (f [0,3] == False) && (f [1,0] == False) && (f [1,1] == False) && (f [1,2] == False) && (f [1,3] == False) && (f [2,0] == True) && (f [2,1] == False) && (f [2,2] == True) && (f [3,0] == False) && (f [3,1] == False) && (f [3,2] == False) && (f [3,3] == False) Output : TIMEOUT *** FIB 96.19s --> Input: \f -> f 1 == 0 && (f 2 == 1) && (f 3 == 1) && (f 4 == 2) && (f 5 == 3) && (f 6 == 5) && (f 7 == 8) Output : \ a -> nat_para a (\ b -> zero) (\ b c d -> nat_para d (\ e -> c e) (\ e f g -> inc (f (f zero))) (inc zero)) zero *** GEQ 0.55s --> Input: \f -> f 0 0 == 1 && (f 0 1 == 0) && (f 1 0 == 1) && (f 1 1 == 1) && (f 1 2 == 0) && (f 2 1 == 1) && (f 2 2 == 1) && (f 2 3 == 0) && (f 3 2 == 1) && (f 3 3 == 1) Output : \ a b -> nat_para b (\ c -> inc zero) (\ c d e -> nat_para e zero (\ f g -> d f)) a *** INSERT timeout --> Input: \f -> f 1 "" == "1" && (f 2 "" == "2") && (f 3 "" == "3") && (f 1 "2" == "1 2") && (f 2 "3 4" == "2 3 4") Output : *** Lasts 7.00s --> Input: \f -> f [[]] == [] && (f ["a"] == "a") && (f ["ab"] == "b") && (f ["abc"] == "c") && (f ["a","b"] == "ab") && (f ["a","bc"] == "ac") && (f ["ab","d"] == "bd") && (f ["ac","bd"] == "cd") && (f ["ac","bd","x"] == "cdx") && (f ["a","bd","x"] == "adx") Output : (\ a -> list_para a nil (\ b c d -> list_para b (\ e f -> e) (\ e f g h i -> g (cons e i) i) nil d)) *** Last 0.05s --> Input: \f -> f [] == Nothing && (f "1" == Just '1') && (f "12" == Just '2') && (f "123" == Just '3') Output : (\ a -> list_para a (\ b -> b) (\ b c d e -> d (just b)) nothing) Output : (\a -> list_para a (\b -> b) (\b c d e -> d (Just b)) Nothing) *** LENGTH 0.008s --> Input: \f -> f [] == 0 && (f ["a"] == 1) && (f ["a", "b"] == 2) && (f ["1","2","3"] == 3) Output : \ a -> list_para a zero (\ b c d -> inc d) *** Member --> Input: \f -> f '1' "" == False && (f '1' "2" == False) && (f '1' "1" == True) && (f '3' "12" == False) && (f '1' "12" == True) && (f '2' "12" == True) && (f '1' "123" == True) && (f '2' "123" == True) && (f '3' "123" == True) && (f '4' "123" == False) Output : *** MULT 5.44s --> Input: \f -> f 0 0 == 0 && (f 0 1 == 0) && (f 1 0 == 0) && (f 1 1 == 1) && (f 2 1 == 2) && (f 2 0 == 0) && (f 0 2 == 0) && (f 2 2 == 4) && (f 2 3 == 6) && (f 3 2 == 6) && (f 3 0 == 0) && (f 0 3 == 0) && (f 4 2 == 8) Output : \ a b -> nat_para b (\ c -> zero) (\ c d e -> nat_para e (\ f -> f) (\ f g h -> inc (g h)) (d e)) a *** Odd/Even --> not possible *** Multfirst 1.3s --> Input: \f -> f "" == "" && (f "a" == "a") && (f "ba" == "bb") && (f "cba" == "ccc") Output : (\ a -> list_para a nil (\ b c d -> cons b (list_para d nil (\ e f g -> cons b g)))) Output Library: (\a -> list_para a a (\b c d -> list_para d [] (\e f g -> b : g))) *** Multlast 0.21s --> Input: \f -> f "" == "" && (f "a" == "a") && (f "ab" == "bb") && (f "abc" == "ccc") Output : (\ a -> list_para a nil (\ b c d -> cons (list_para d b (\ e f g -> e)) d)) Output Library: (\a -> list_para a [] (\b c d -> list_para d b (\e f g -> e) : d)) *** ODD 0.06s --> Input: \f -> f 0 == 0 && (f 1 == 1) && (f 2 == 0) && (f 3 == 1) Output : \ a -> nat_para a zero (\ b c -> nat_para c (inc zero) (\ d e -> zero)) *** ODDPOS 4.01s --> Input: \f -> f [] == [] && (f [1] == [1]) && (f [1,2] == [1]) && (f [1,2,3] == [1,3]) && (f [1,2,3,4] == [1,3]) Output : \ a -> list_para a (\ b -> nil) (\ b c d e -> nat_para e (cons b (d b)) (\ f g -> d zero)) zero *** Oddslist timeout --> Input: \f -> f [] == True && (f [0] == False) && (f [1] == True) && (f [2] == False) && (f [3] == True) && (f [0,0] == False) && (f [0,1] == False) && (f [0,2] == False) && (f [0,3] == False) && (f [1,0] == False) && (f [1,1] == True) && (f [1,2] == False) && (f [1,3] == True) && (f [2,0] == False) && (f [2,1] == False) && (f [2,2] == False) && (f [2,2] == False) && (f [3,0] == False) && (f [3,1] == True) && (f [3,2] == False) && (f [3,3] == True) Output : TIMEOUT *** Reverse 0.08s --> Input: \f -> f "" == "" && (f "1" == "1") && (f "12" == "21") && (f "123" == "321") Output : (\ a -> list_para a (\ b -> b) (\ b c d e -> d (cons b e)) nil) *** Shiftl 1.32s --> Input: \f -> f "" == "" && (f "1" == "1") && (f "12" == "21") && (f "123" == "231") && (f "1234" == "2341") Output : (\ a -> list_para a nil (\ b c d -> cons (incr (list_para d zero (\ e f g -> b))) d)) *** Shiftr 4.93s --> Input: \f -> f "" == "" && (f "1" == "1") && (f "12" == "21") && (f "123" == "312") && (f "1234" == "4123") Output :(\ a -> list_para a (\ b -> nil) (\ b c d e -> cons e (d b)) (list_para a zero (\ b c d -> incr d))) *** Sort timeout --> Input: \f -> f [] == [] && (f [1] == [1]) && (f [0,1] == [0,1]) && (f [0,2] == [0,2]) && (f [1,0] == [0,1]) && (f [1,2] == [1,2]) && (f [2,0] == [0,2]) && (f [2,1] == [1,2]) && (f [0,1,2] == [0,1,2]) && (f [0,2,1] == [0,1,2]) && (f [1,0,2] == [0,1,2]) && (f [1,2,0] == [0,1,2]) && (f [2,0,1] == [0,1,2]) && (f [2,1,0] == [0,1,2]) Output : TIMEOUT *** SUM 0.49s --> Input: \f -> f [] == 0 && (f [1] == 1) && (f [2] == 2) && (f [1,2] == 3) && (f [1,0] == 1) && (f [1,2,3] == 6) Output : (\ a -> list_para a zero (\ b c d -> nat_para d (\ e -> e) (\ e f g -> inc (f g)) b)) *** SWAP timeout --> Input: \f -> f [] == [] && (f [1] == [1]) && (f [2] == [2]) && (f [1,2] == [2,1]) && (f [1,5,3] == [3,5,1]) && (f [1,2,3,4] == [4,2,3,1]) Output : TIMEOUT *** SWITCH timeout --> Input: \f -> f [] == [] && (f [1] == [1]) && (f [2] == [2]) && (f [1,2] == [2,1]) && (f [1,5,3] == [5,1,3]) && (f [1,2,3,4] == [2,1,4,3]) && (f [1,2,3,4,5] == [2,1,4,3,5]) && (f [1,2,3,4,5,6] == [2,1,4,3,6,5]) Output : TIMEOUT *** TAKE 0.05s --> Input: \f -> f 0 [] == [] && (f 0 [1] == [1]) && (f 0 [2] == [2]) && (f 1 [1] == []) && (f 1 [2] == []) && (f 1 [1,2] == [2]) && (f 1 [1,2,3] == [2,3]) && (f 2 [1,2] == []) && (f 2 [1,2,3] == [3]) Output : \ a b -> nat_para a b (\ c d -> list_para d nil (\ e f g -> f)) *** Weave timeout | 30.59s --> Input: \f -> f "" "" == "" && (f "a" "" == "a") && (f "" "1" == "1") && (f "a" "1" == "a1") && (f "ab" "1" == "a1b") && (f "a" "12" == "a12") && (f "" "12" == "12") && (f "ab" "" == "ab") && (f "ab" "12" == "a1b2") Output :(\ a b -> list_para a (\ c -> c) (\ c d e f -> cons c (list_para f (e nil) (\ g h i -> cons g (e h)))) b)