This translation extends 'word_prelude'. Certificate theorem for GETKEYS: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "GETKEYS") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE a (PAIR_TYPE b (PAIR_TYPE c (PAIR_TYPE d (PAIR_TYPE e (PAIR_TYPE f (PAIR_TYPE g (PAIR_TYPE h (PAIR_TYPE i (PAIR_TYPE j (PAIR_TYPE k (PAIR_TYPE l (PAIR_TYPE m (PAIR_TYPE n (PAIR_TYPE $o (PAIR_TYPE p (PAIR_TYPE q (PAIR_TYPE r (PAIR_TYPE s (PAIR_TYPE t (PAIR_TYPE u (PAIR_TYPE v (PAIR_TYPE w (PAIR_TYPE x (PAIR_TYPE y (PAIR_TYPE z (PAIR_TYPE a0 (PAIR_TYPE a1 (PAIR_TYPE a2 (PAIR_TYPE a3 (PAIR_TYPE a4 (PAIR_TYPE a5 (PAIR_TYPE a6 (PAIR_TYPE a7 (PAIR_TYPE a8 (PAIR_TYPE a9 (PAIR_TYPE a10 (PAIR_TYPE a11 (PAIR_TYPE a12 (PAIR_TYPE a13 (PAIR_TYPE a14 a15)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD WORD) GETKEYS) Certificate theorem for PreWhitening: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "PreWhitening") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) PreWhitening) Certificate theorem for ROTKEYS: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "ROTKEYS") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))))))))))))))))))))))))))))) ROTKEYS) Certificate theorem for InvPostWhitening: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "InvPostWhitening") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) InvPostWhitening) Certificate theorem for InvPreWhitening: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "InvPreWhitening") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) InvPreWhitening) Certificate theorem for RightShift: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "RightShift") ((WORD --> WORD --> WORD) $>>>) Certificate theorem for LeftShift: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "LeftShift") ((WORD --> WORD --> WORD) $<<<) Certificate theorem for CompUT: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "CompUT") ((WORD --> WORD) CompUT) Certificate theorem for FwdRound: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "FwdRound") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD WORD --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) FwdRound) Certificate theorem for BwdRound: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "BwdRound") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD WORD --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) BwdRound) Certificate theorem for PostWhitening: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "PostWhitening") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) PostWhitening) Certificate theorem for Round: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "Round") ((NUM --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) Round) Certificate theorem for InvRound: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "InvRound") ((NUM --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) InvRound) Certificate theorem for r: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "r") (NUM r) Certificate theorem for RC6_FWD: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "RC6_FWD") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) RC6_FWD) Certificate theorem for RC6_BWD: |- DeclAssum example_rc6_decls env ⇒ Eval env (Var "RC6_BWD") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) RC6_BWD) Definition of declaration list: |- example_rc6_decls = [Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])]; Dtype [(["a"],"list", [("Cons",[Tvar "a"; Tapp [Tvar "a"] "list"]); ("Nil",[])])]; Dlet (Pvar "HD") (Fun "x1" (Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")])); Dlet (Pvar "TL") (Fun "x1" (Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v1")])); Dletrec [("APPEND","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "APPEND") (Var "v1")) (Var "v4")])]))]; Dletrec [("REV","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Cons" [Var "v2"; Var "v4"]))]))]; Dlet (Pvar "REVERSE") (Fun "v1" (App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Nil" []))); Dlet (Pvar "FST") (Fun "v3" (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v2")])); Dlet (Pvar "SND") (Fun "v3" (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v1")])); Dlet (Pvar "CURRY") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (Var "v1") (Con "Pair" [Var "v2"; Var "v3"]))))); Dlet (Pvar "UNCURRY") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "v1") (App Opapp (Var "FST") (Var "v2"))) (App Opapp (Var "SND") (Var "v2"))))); Dlet (Pvar "o") (Fun "v2" (Fun "v3" (Fun "v1" (App Opapp (Var "v2") (App Opapp (Var "v3") (Var "v1")))))); Dlet (Pvar "I") (Fun "v1" (Var "v1")); Dlet (Pvar "C") (Fun "v3" (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v3") (Var "v1")) (Var "v2"))))); Dlet (Pvar "K") (Fun "v2" (Fun "v1" (Var "v2"))); Dlet (Pvar "S") (Fun "v3" (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v3") (Var "v1")) (App Opapp (Var "v2") (Var "v1")))))); Dlet (Pvar "UPDATE") (Fun "v3" (Fun "v4" (Fun "v2" (Fun "v1" (If (App Equality (Var "v3") (Var "v1")) (Var "v4") (App Opapp (Var "v2") (Var "v1"))))))); Dlet (Pvar "W") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v2") (Var "v1")) (Var "v1")))); Dtype [([],"one",[("One",[])])]; Dtype [(["a"],"option",[("Some",[Tvar "a"]); ("None",[])])]; Dlet (Pvar "THE") (Fun "x1" (Mat (Var "x1") [(Pcon "None" [],Raise Bind_error); (Pcon "Some" [Pvar "v1"],Var "v1")])); Dlet (Pvar "IS_NONE") (Fun "v2" (Mat (Var "v2") [(Pcon "None" [],Val (Lit (Bool T))); (Pcon "Some" [Pvar "v1"],Val (Lit (Bool F)))])); Dlet (Pvar "IS_SOME") (Fun "v2" (Mat (Var "v2") [(Pcon "None" [],Val (Lit (Bool F))); (Pcon "Some" [Pvar "v1"],Val (Lit (Bool T)))])); Dlet (Pvar "OPTION_MAP") (Fun "v2" (Fun "v3" (Mat (Var "v3") [(Pcon "None" [],Con "None" []); (Pcon "Some" [Pvar "v1"], Con "Some" [App Opapp (Var "v2") (Var "v1")])]))); Dlet (Pvar "OPTION_MAP2") (Fun "v1" (Fun "v2" (Fun "v3" (If (Log And (App Opapp (Var "IS_SOME") (Var "v2")) (App Opapp (Var "IS_SOME") (Var "v3"))) (Con "Some" [App Opapp (App Opapp (Var "v1") (App Opapp (Var "THE") (Var "v2"))) (App Opapp (Var "THE") (Var "v3"))]) (Con "None" []))))); Dtype [(["a"; "b"],"sum",[("Inr",[Tvar "b"]); ("Inl",[Tvar "a"])])]; Dlet (Pvar "ISL") (Fun "v3" (Mat (Var "v3") [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool T))); (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool F)))])); Dlet (Pvar "ISR") (Fun "v3" (Mat (Var "v3") [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool F))); (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool T)))])); Dlet (Pvar "OUTL") (Fun "x1" (Mat (Var "x1") [(Pcon "Inl" [Pvar "v1"],Var "v1"); (Pcon "Inr" [Pvar "v2"],Raise Bind_error)])); Dlet (Pvar "OUTR") (Fun "x1" (Mat (Var "x1") [(Pcon "Inl" [Pvar "v1"],Raise Bind_error); (Pcon "Inr" [Pvar "v2"],Var "v2")])); Dlet (Pvar "++") (Fun "v3" (Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Inl" [Pvar "v1"], Con "Inl" [App Opapp (Var "v3") (Var "v1")]); (Pcon "Inr" [Pvar "v2"], Con "Inr" [App Opapp (Var "v4") (Var "v2")])])))); Dletrec [("LENGTH_AUX","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1")) (App (Opn Plus) (Var "v4") (Val (Lit (IntLit 1)))))]))]; Dlet (Pvar "LENGTH") (Fun "v1" (App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1")) (Val (Lit (IntLit 0))))); Dletrec [("MAP","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [App Opapp (Var "v3") (Var "v2"); App Opapp (App Opapp (Var "MAP") (Var "v3")) (Var "v1")])]))]; Dletrec [("FILTER","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Opapp (Var "v3") (Var "v2")) (Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "FILTER") (Var "v3")) (Var "v1")]) (App Opapp (App Opapp (Var "FILTER") (Var "v3")) (Var "v1")))]))]; Dletrec [("FOLDR","v3", Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (App Opapp (Var "FOLDR") (Var "v3")) (Var "v4")) (Var "v1")))])))]; Dletrec [("FOLDL","v3", Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (App Opapp (Var "FOLDL") (Var "v3")) (App Opapp (App Opapp (Var "v3") (Var "v4")) (Var "v2"))) (Var "v1"))])))]; Dletrec [("SUM","v3", Mat (Var "v3") [(Pcon "Nil" [],Val (Lit (IntLit 0))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App (Opn Plus) (Var "v2") (App Opapp (Var "SUM") (Var "v1")))])]; Dletrec [("UNZIP","v3", Mat (Var "v3") [(Pcon "Nil" [],Con "Pair" [Con "Nil" []; Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Pair" [Con "Cons" [App Opapp (Var "FST") (Var "v2"); App Opapp (Var "FST") (App Opapp (Var "UNZIP") (Var "v1"))]; Con "Cons" [App Opapp (Var "SND") (Var "v2"); App Opapp (Var "SND") (App Opapp (Var "UNZIP") (Var "v1"))]])])]; Dletrec [("FLAT","v3", Mat (Var "v3") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "APPEND") (Var "v2")) (App Opapp (Var "FLAT") (Var "v1")))])]; Dletrec [("TAKE","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Con "Nil" []) (Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "TAKE") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (Var "v1")]))]))]; Dletrec [("DROP","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Con "Cons" [Var "v2"; Var "v1"]) (App Opapp (App Opapp (Var "DROP") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (Var "v1")))]))]; Dletrec [("SNOC","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Cons" [Var "v3"; Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "SNOC") (Var "v3")) (Var "v1")])]))]; Dletrec [("EVERY","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "EVERY") (Var "v3")) (Var "v1")))]))]; Dletrec [("EXISTS","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log Or (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "EXISTS") (Var "v3")) (Var "v1")))]))]; Dletrec [("GENLIST","v1", Fun "v2" (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0)))) (Con "Nil" []) (App Opapp (App Opapp (Var "SNOC") (App Opapp (Var "v1") (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1)))))) (App Opapp (App Opapp (Var "GENLIST") (Var "v1")) (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1))))))))]; Dlet (Pvar "PAD_RIGHT") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (App Opapp (Var "APPEND") (Var "v3")) (App Opapp (App Opapp (Var "GENLIST") (App Opapp (Var "K") (Var "v1"))) (Let "k" (App (Opn Minus) (Var "v2") (App Opapp (Var "LENGTH") (Var "v3"))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))))); Dlet (Pvar "PAD_LEFT") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "GENLIST") (App Opapp (Var "K") (Var "v1"))) (Let "k" (App (Opn Minus) (Var "v2") (App Opapp (Var "LENGTH") (Var "v3"))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (Var "v3"))))); Dletrec [("MEM","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log Or (App Equality (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "MEM") (Var "v3")) (Var "v1")))]))]; Dletrec [("ALL_DISTINCT","v3", Mat (Var "v3") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Equality (App Opapp (App Opapp (Var "MEM") (Var "v2")) (Var "v1")) (Val (Lit (Bool F)))) (App Opapp (Var "ALL_DISTINCT") (Var "v1")))])]; Dletrec [("isPREFIX","v5", Fun "v6" (Mat (Var "v5") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Mat (Var "v6") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Equality (Var "v4") (Var "v2")) (App Opapp (App Opapp (Var "isPREFIX") (Var "v3")) (Var "v1")))])]))]; Dletrec [("FRONT","x1", Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v1") (Con "Nil" [])) (Con "Nil" []) (Con "Cons" [Var "v2"; App Opapp (Var "FRONT") (Var "v1")]))])]; Dletrec [("ZIP","x1", Mat (Var "x1") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v8") [(Pcon "Nil" [], Mat (Var "v7") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Raise Bind_error)]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v7") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Con "Cons" [Con "Pair" [Var "v6"; Var "v4"]; App Opapp (Var "ZIP") (Con "Pair" [Var "v5"; Var "v3"])])])])])]; Dletrec [("EL","v1", Fun "v2" (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0)))) (App Opapp (Var "HD") (Var "v2")) (App Opapp (App Opapp (Var "EL") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (App Opapp (Var "TL") (Var "v2")))))]; Dletrec [("PART","v3", Fun "v4" (Fun "v5" (Fun "v6" (Mat (Var "v4") [(Pcon "Nil" [],Con "Pair" [Var "v5"; Var "v6"]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Con "Cons" [Var "v2"; Var "v5"])) (Var "v6")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Var "v5")) (Con "Cons" [Var "v2"; Var "v6"])))]))))]; Dlet (Pvar "PARTITION") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v1")) (Var "v2")) (Con "Nil" [])) (Con "Nil" [])))); Dletrec [("QSORT","v7", Fun "v8" (Mat (Var "v8") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Let "v3" (App Opapp (App Opapp (Var "PARTITION") (Fun "v4" (App Opapp (App Opapp (Var "v7") (Var "v4")) (Var "v6")))) (Var "v5")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v2"))) (Con "Cons" [Var "v6"; Con "Nil" []]))) (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v1")))]))]))]; Dletrec [("EXP_AUX","v2", Fun "v3" (Fun "v1" (If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Var "v1") (App Opapp (App Opapp (App Opapp (Var "EXP_AUX") (Var "v2")) (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (App (Opn Times) (Var "v2") (Var "v1"))))))]; Dlet (Pvar "EXP") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (Var "EXP_AUX") (Var "v1")) (Var "v2")) (Val (Lit (IntLit 1)))))); Dlet (Pvar "MIN") (Fun "v1" (Fun "v2" (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v1") (Var "v2")))); Dlet (Pvar "MAX") (Fun "v1" (Fun "v2" (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v2") (Var "v1")))); Dlet (Pvar "EVEN") (Fun "v1" (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0))))); Dlet (Pvar "ODD") (Fun "v1" (App (Opb Lt) (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))))); Dletrec [("FUNPOW","v1", Fun "v2" (Fun "v3" (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0)))) (Var "v3") (App Opapp (App Opapp (App Opapp (Var "FUNPOW") (Var "v1")) (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1))))) (App Opapp (Var "v1") (Var "v3"))))))]; Dlet (Pvar "MOD_2EXP") (Fun "v2" (Fun "v1" (App (Opn Modulo) (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2"))))); Dlet (Pvar "DIV_2EXP") (Fun "v2" (Fun "v1" (App (Opn Divide) (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2"))))); Dlet (Pvar "PRE") (Fun "v1" (Let "k" (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))); Dlet (Pvar "ABS_DIFF") (Fun "v2" (Fun "v1" (If (App (Opb Lt) (Var "v2") (Var "v1")) (Let "k" (App (Opn Minus) (Var "v1") (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (Let "k" (App (Opn Minus) (Var "v2") (Var "v1")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))); Dlet (Pvar "DIV2") (Fun "v1" (App (Opn Divide) (Var "v1") (Val (Lit (IntLit 2))))); Dletrec [("string_lt","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Nil" [], Mat (Var "v8") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Val (Lit (Bool T)))]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v8") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Log Or (App Opapp (Let "m" (Var "v6") (Fun "n" (App (Opb Lt) (Var "m") (Var "n")))) (Var "v4")) (Log And (App Equality (Var "v6") (Var "v4")) (App Opapp (App Opapp (Var "string_lt") (Var "v5")) (Var "v3"))))])]))]; Dlet (Pvar "string_le") (Fun "v1" (Fun "v2" (Log Or (App Equality (Var "v1") (Var "v2")) (App Opapp (App Opapp (Var "string_lt") (Var "v1")) (Var "v2"))))); Dlet (Pvar "string_gt") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "string_lt") (Var "v2")) (Var "v1")))); Dlet (Pvar "string_ge") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "string_le") (Var "v2")) (Var "v1")))); Dlet (Pvar "BITS") (Fun "v1" (Fun "v2" (Fun "v3" (App (Opn Divide) (App (Opn Modulo) (Var "v3") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (App (Opn Plus) (Var "v1") (Val (Lit (IntLit 1)))))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")))))); Dlet (Pvar "BIT") (Fun "v1" (Fun "v2" (App Equality (App (Opn Modulo) (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 1)))))); Dlet (Pvar "SBIT") (Fun "v1" (Fun "v2" (If (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (Val (Lit (IntLit 0)))))); Dtype [(["a"],"ptree", [("Branch", [Tnum; Tnum; Tapp [Tvar "a"] "ptree"; Tapp [Tvar "a"] "ptree"]); ("Leaf",[Tnum; Tvar "a"]); ("Empty",[])])]; Dletrec [("BRANCHING_BIT","v1", Fun "v2" (If (Log Or (App Equality (App Opapp (Var "ODD") (Var "v1")) (App Opapp (Var "EVEN") (Var "v2"))) (App Equality (Var "v1") (Var "v2"))) (Val (Lit (IntLit 0))) (App (Opn Plus) (App Opapp (App Opapp (Var "BRANCHING_BIT") (App Opapp (Var "DIV2") (Var "v1"))) (App Opapp (Var "DIV2") (Var "v2"))) (Val (Lit (IntLit 1))))))]; Dletrec [("PEEK","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Empty" [],Con "None" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v8") (Var "v2")) (Con "Some" [Var "v1"]) (Con "None" [])); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], App Opapp (App Opapp (Var "PEEK") (If (App Opapp (App Opapp (Var "BIT") (Var "v5")) (Var "v8")) (Var "v4") (Var "v3"))) (Var "v8"))]))]; Dlet (Pvar "MOD_2EXP_EQ") (Fun "v3" (Fun "v1" (Fun "v2" (App Equality (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3")) (Var "v1")) (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3")) (Var "v2")))))); Dlet (Pvar "JOIN") (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v7"; Pvar "v6"], Mat (Var "v6") [(Pcon "Pair" [Pvar "v5"; Pvar "v4"], Mat (Var "v4") [(Pcon "Pair" [Pvar "v3"; Pvar "v2"], Let "v1" (App Opapp (App Opapp (Var "BRANCHING_BIT") (Var "v7")) (Var "v3")) (If (App Opapp (App Opapp (Var "BIT") (Var "v1")) (Var "v7")) (Con "Branch" [App Opapp (App Opapp (Var "MOD_2EXP") (Var "v1")) (Var "v7"); Var "v1"; Var "v5"; Var "v2"]) (Con "Branch" [App Opapp (App Opapp (Var "MOD_2EXP") (Var "v1")) (Var "v7"); Var "v1"; Var "v2"; Var "v5"])))])])])); Dletrec [("ADD","v13", Fun "v14" (Mat (Var "v13") [(Pcon "Empty" [], Mat (Var "v14") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Leaf" [Var "v2"; Var "v1"])]); (Pcon "Leaf" [Pvar "v6"; Pvar "v5"], Mat (Var "v14") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], If (App Equality (Var "v6") (Var "v4")) (Con "Leaf" [Var "v4"; Var "v3"]) (App Opapp (Var "JOIN") (Con "Pair" [Var "v4"; Con "Pair" [Con "Leaf" [Var "v4"; Var "v3"]; Con "Pair" [Var "v6"; Con "Leaf" [Var "v6"; Var "v5"]]]])))]); (Pcon "Branch" [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"], Mat (Var "v14") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], If (App Opapp (App Opapp (App Opapp (Var "MOD_2EXP_EQ") (Var "v11")) (Var "v8")) (Var "v12")) (If (App Opapp (App Opapp (Var "BIT") (Var "v11")) (Var "v8")) (Con "Branch" [Var "v12"; Var "v11"; App Opapp (App Opapp (Var "ADD") (Var "v10")) (Con "Pair" [Var "v8"; Var "v7"]); Var "v9"]) (Con "Branch" [Var "v12"; Var "v11"; Var "v10"; App Opapp (App Opapp (Var "ADD") (Var "v9")) (Con "Pair" [Var "v8"; Var "v7"])])) (App Opapp (Var "JOIN") (Con "Pair" [Var "v8"; Con "Pair" [Con "Leaf" [Var "v8"; Var "v7"]; Con "Pair" [Var "v12"; Con "Branch" [Var "v12"; Var "v11"; Var "v10"; Var "v9"]]]])))])]))]; Dlet (Pvar "BRANCH") (Fun "v31" (Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v26") [(Pcon "Empty" [], Mat (Var "v25") [(Pcon "Empty" [],Con "Empty" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], Con "Leaf" [Var "v2"; Var "v1"]); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], Con "Branch" [Var "v6"; Var "v5"; Var "v4"; Var "v3"])]); (Pcon "Leaf" [Pvar "v14"; Pvar "v13"], Mat (Var "v25") [(Pcon "Empty" [], Con "Leaf" [Var "v14"; Var "v13"]); (Pcon "Leaf" [Pvar "v8"; Pvar "v7"], Con "Branch" [Var "v30"; Var "v28"; Con "Leaf" [Var "v14"; Var "v13"]; Con "Leaf" [Var "v8"; Var "v7"]]); (Pcon "Branch" [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"], Con "Branch" [Var "v30"; Var "v28"; Con "Leaf" [Var "v14"; Var "v13"]; Con "Branch" [Var "v12"; Var "v11"; Var "v10"; Var "v9"]])]); (Pcon "Branch" [Pvar "v24"; Pvar "v23"; Pvar "v22"; Pvar "v21"], Mat (Var "v25") [(Pcon "Empty" [], Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]); (Pcon "Leaf" [Pvar "v16"; Pvar "v15"], Con "Branch" [Var "v30"; Var "v28"; Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]; Con "Leaf" [Var "v16"; Var "v15"]]); (Pcon "Branch" [Pvar "v20"; Pvar "v19"; Pvar "v18"; Pvar "v17"], Con "Branch" [Var "v30"; Var "v28"; Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]; Con "Branch" [Var "v20"; Var "v19"; Var "v18"; Var "v17"]])])])])])])); Dletrec [("REMOVE","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Empty" [],Con "Empty" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v2") (Var "v8")) (Con "Empty" []) (Con "Leaf" [Var "v2"; Var "v1"])); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], If (App Opapp (App Opapp (App Opapp (Var "MOD_2EXP_EQ") (Var "v5")) (Var "v8")) (Var "v6")) (If (App Opapp (App Opapp (Var "BIT") (Var "v5")) (Var "v8")) (App Opapp (Var "BRANCH") (Con "Pair" [Var "v6"; Con "Pair" [Var "v5"; Con "Pair" [App Opapp (App Opapp (Var "REMOVE") (Var "v4")) (Var "v8"); Var "v3"]]])) (App Opapp (Var "BRANCH") (Con "Pair" [Var "v6"; Con "Pair" [Var "v5"; Con "Pair" [Var "v4"; App Opapp (App Opapp (Var "REMOVE") (Var "v3")) (Var "v8")]]]))) (Con "Branch" [Var "v6"; Var "v5"; Var "v4"; Var "v3"]))]))]; Dlet (Pvar "word_add") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_mul") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_add_1") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_mul_1") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_add_2") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_mul_2") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dletrec [("BITWISE","v1", Fun "v2" (Fun "v3" (Fun "v4" (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (App (Opn Plus) (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v2")) (Var "v3")) (Var "v4")) (App Opapp (App Opapp (Var "SBIT") (App Opapp (App Opapp (Var "v2") (App Opapp (App Opapp (Var "BIT") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v3"))) (App Opapp (App Opapp (Var "BIT") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v4")))) (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))))))))]; Dlet (Pvar "word_xor") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_xor_1") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 8)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_xor_2") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_or") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (Log Or (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_or_1") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16)))) (Fun "v2" (Fun "v1" (Log Or (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_and") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (Log And (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_lsl") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (Var "v1")))); Dlet (Pvar "word_lsl_1") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul_1") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))) (Var "v1")))); Dlet (Pvar "word_lsl_2") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul_2") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1")))); Dlet (Pvar "word_lsr") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_lsr_1") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_lsr_2") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_msb") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 31)))) (Var "v1"))); Dlet (Pvar "word_msb_1") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 15)))) (Var "v1"))); Dlet (Pvar "word_msb_2") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 7)))) (Var "v1"))); Dlet (Pvar "word_lsb") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_lsb_1") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_lsb_2") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_asr") (Fun "v2" (Fun "v1" (If (App Opapp (Var "word_msb") (Var "v2")) (App Opapp (App Opapp (Var "word_or") (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 4294967296))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 32))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (App Opapp (App Opapp (Var "word_lsr") (Var "v2")) (Var "v1"))) (App Opapp (App Opapp (Var "word_lsr") (Var "v2")) (Var "v1"))))); Dlet (Pvar "word_asr_1") (Fun "v2" (Fun "v1" (If (App Opapp (Var "word_msb_1") (Var "v2")) (App Opapp (App Opapp (Var "word_or_1") (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 65536))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 16))) (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 16))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))) (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2")) (Var "v1"))) (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2")) (Var "v1"))))); Dlet (Pvar "word_sub") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 4294967296))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))))); Dlet (Pvar "word_sub_1") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add_1") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 65536))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))); Dlet (Pvar "word_sub_2") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add_2") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 256))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))); Dlet (Pvar "word_bits") (Fun "v1" (Fun "v2" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (Var "BITS") (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 31))))) (Var "v2")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))))); Dlet (Pvar "word_ror") (Fun "v3" (Fun "v2" (Let "v1" (App (Opn Modulo) (Var "v2") (Val (Lit (IntLit 32)))) (App Opapp (App Opapp (Var "word_or") (App Opapp (App Opapp (App Opapp (Var "word_bits") (Val (Lit (IntLit 31)))) (Var "v1")) (Var "v3"))) (App Opapp (App Opapp (Var "word_lsl") (App Opapp (App Opapp (App Opapp (Var "word_bits") (Let "k" (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))) (Val (Lit (IntLit 0)))) (Var "v3"))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (Var "v1")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))))); Dlet (Pvar "word_rol") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "word_ror") (Var "v2")) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 32))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))); Dlet (Pvar "GETKEYS") (Fun "v87" (Mat (Var "v87") [(Pcon "Pair" [Pvar "v86"; Pvar "v85"], Mat (Var "v85") [(Pcon "Pair" [Pvar "v84"; Pvar "v83"], Mat (Var "v83") [(Pcon "Pair" [Pvar "v82"; Pvar "v81"], Mat (Var "v81") [(Pcon "Pair" [Pvar "v80"; Pvar "v79"], Mat (Var "v79") [(Pcon "Pair" [Pvar "v78"; Pvar "v77"], Mat (Var "v77") [(Pcon "Pair" [Pvar "v76"; Pvar "v75"], Mat (Var "v75") [(Pcon "Pair" [Pvar "v74"; Pvar "v73"], Mat (Var "v73") [(Pcon "Pair" [Pvar "v72"; Pvar "v71"], Mat (Var "v71") [(Pcon "Pair" [Pvar "v70"; Pvar "v69"], Mat (Var "v69") [(Pcon "Pair" [Pvar "v68"; Pvar "v67"], Mat (Var "v67") [(Pcon "Pair" [Pvar "v66"; Pvar "v65"], Mat (Var "v65") [(Pcon "Pair" [Pvar "v64"; Pvar "v63"], Mat (Var "v63") [(Pcon "Pair" [Pvar "v62"; Pvar "v61"], Mat (Var "v61") [(Pcon "Pair" [Pvar "v60"; Pvar "v59"], Mat (Var "v59") [(Pcon "Pair" [Pvar "v58"; Pvar "v57"], Mat (Var "v57") [(Pcon "Pair" [Pvar "v56"; Pvar "v55"], Mat (Var "v55") [(Pcon "Pair" [Pvar "v54"; Pvar "v53"], Mat (Var "v53") [(Pcon "Pair" [Pvar "v52"; Pvar "v51"], Mat (Var "v51") [(Pcon "Pair" [Pvar "v50"; Pvar "v49"], Mat (Var "v49") [(Pcon "Pair" [Pvar "v48"; Pvar "v47"], Mat (Var "v47") [(Pcon "Pair" [Pvar "v46"; Pvar "v45"], Mat (Var "v45") [(Pcon "Pair" [Pvar "v44"; Pvar "v43"], Mat (Var "v43") [(Pcon "Pair" [Pvar "v42"; Pvar "v41"], Mat (Var "v41") [(Pcon "Pair" [Pvar "v40"; Pvar "v39"], Mat (Var "v39") [(Pcon "Pair" [Pvar "v38"; Pvar "v37"], Mat (Var "v37") [(Pcon "Pair" [Pvar "v36"; Pvar "v35"], Mat (Var "v35") [(Pcon "Pair" [Pvar "v34"; Pvar "v33"], Mat (Var "v33") [(Pcon "Pair" [Pvar "v32"; Pvar "v31"], Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v86"; Var "v84"])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])); Dlet (Pvar "PreWhitening") (Fun "v7" (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v6"; Con "Pair" [App Opapp (App Opapp (Var "word_add") (Var "v4")) (App Opapp (Var "FST") (App Opapp (Var "GETKEYS") (Var "v7"))); Con "Pair" [Var "v2"; App Opapp (App Opapp (Var "word_add") (Var "v1")) (App Opapp (Var "SND") (App Opapp (Var "GETKEYS") (Var "v7")))]]])])])]))); Dlet (Pvar "ROTKEYS") (Fun "v87" (Mat (Var "v87") [(Pcon "Pair" [Pvar "v86"; Pvar "v85"], Mat (Var "v85") [(Pcon "Pair" [Pvar "v84"; Pvar "v83"], Mat (Var "v83") [(Pcon "Pair" [Pvar "v82"; Pvar "v81"], Mat (Var "v81") [(Pcon "Pair" [Pvar "v80"; Pvar "v79"], Mat (Var "v79") [(Pcon "Pair" [Pvar "v78"; Pvar "v77"], Mat (Var "v77") [(Pcon "Pair" [Pvar "v76"; Pvar "v75"], Mat (Var "v75") [(Pcon "Pair" [Pvar "v74"; Pvar "v73"], Mat (Var "v73") [(Pcon "Pair" [Pvar "v72"; Pvar "v71"], Mat (Var "v71") [(Pcon "Pair" [Pvar "v70"; Pvar "v69"], Mat (Var "v69") [(Pcon "Pair" [Pvar "v68"; Pvar "v67"], Mat (Var "v67") [(Pcon "Pair" [Pvar "v66"; Pvar "v65"], Mat (Var "v65") [(Pcon "Pair" [Pvar "v64"; Pvar "v63"], Mat (Var "v63") [(Pcon "Pair" [Pvar "v62"; Pvar "v61"], Mat (Var "v61") [(Pcon "Pair" [Pvar "v60"; Pvar "v59"], Mat (Var "v59") [(Pcon "Pair" [Pvar "v58"; Pvar "v57"], Mat (Var "v57") [(Pcon "Pair" [Pvar "v56"; Pvar "v55"], Mat (Var "v55") [(Pcon "Pair" [Pvar "v54"; Pvar "v53"], Mat (Var "v53") [(Pcon "Pair" [Pvar "v52"; Pvar "v51"], Mat (Var "v51") [(Pcon "Pair" [Pvar "v50"; Pvar "v49"], Mat (Var "v49") [(Pcon "Pair" [Pvar "v48"; Pvar "v47"], Mat (Var "v47") [(Pcon "Pair" [Pvar "v46"; Pvar "v45"], Mat (Var "v45") [(Pcon "Pair" [Pvar "v44"; Pvar "v43"], Mat (Var "v43") [(Pcon "Pair" [Pvar "v42"; Pvar "v41"], Mat (Var "v41") [(Pcon "Pair" [Pvar "v40"; Pvar "v39"], Mat (Var "v39") [(Pcon "Pair" [Pvar "v38"; Pvar "v37"], Mat (Var "v37") [(Pcon "Pair" [Pvar "v36"; Pvar "v35"], Mat (Var "v35") [(Pcon "Pair" [Pvar "v34"; Pvar "v33"], Mat (Var "v33") [(Pcon "Pair" [Pvar "v32"; Pvar "v31"], Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v82"; Con "Pair" [Var "v80"; Con "Pair" [Var "v78"; Con "Pair" [Var "v76"; Con "Pair" [Var "v74"; Con "Pair" [Var "v72"; Con "Pair" [Var "v70"; Con "Pair" [Var "v68"; Con "Pair" [Var "v66"; Con "Pair" [Var "v64"; Con "Pair" [Var "v62"; Con "Pair" [Var "v60"; Con "Pair" [Var "v58"; Con "Pair" [Var "v56"; Con "Pair" [Var "v54"; Con "Pair" [Var "v52"; Con "Pair" [Var "v50"; Con "Pair" [Var "v48"; Con "Pair" [Var "v46"; Con "Pair" [Var "v44"; Con "Pair" [Var "v42"; Con "Pair" [Var "v40"; Con "Pair" [Var "v38"; Con "Pair" [Var "v36"; Con "Pair" [Var "v34"; Con "Pair" [Var "v32"; Con "Pair" [Var "v30"; Con "Pair" [Var "v28"; Con "Pair" [Var "v26"; Con "Pair" [Var "v24"; Con "Pair" [Var "v22"; Con "Pair" [Var "v20"; Con "Pair" [Var "v18"; Con "Pair" [Var "v16"; Con "Pair" [Var "v14"; Con "Pair" [Var "v12"; Con "Pair" [Var "v10"; Con "Pair" [Var "v8"; Con "Pair" [Var "v6"; Con "Pair" [Var "v4"; Con "Pair" [Var "v2"; Con "Pair" [Var "v1"; Con "Pair" [Var "v86"; Var "v84"]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])); Dlet (Pvar "InvPostWhitening") (Fun "v7" (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v6"; Con "Pair" [App Opapp (App Opapp (Var "word_sub") (Var "v4")) (App Opapp (Var "FST") (App Opapp (Var "GETKEYS") (Var "v7"))); Con "Pair" [Var "v2"; App Opapp (App Opapp (Var "word_sub") (Var "v1")) (App Opapp (Var "SND") (App Opapp (Var "GETKEYS") (Var "v7")))]]])])])]))); Dlet (Pvar "InvPreWhitening") (Fun "v7" (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Opapp (App Opapp (Var "word_sub") (Var "v6")) (App Opapp (Var "SND") (App Opapp (Var "GETKEYS") (Var "v7"))); Con "Pair" [Var "v4"; Con "Pair" [App Opapp (App Opapp (Var "word_sub") (Var "v2")) (App Opapp (Var "SND") (App Opapp (Var "GETKEYS") (Var "v7"))); Var "v1"]]])])])]))); Dlet (Pvar "RightShift") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "word_ror") (Var "v2")) (Var "v1")))); Dlet (Pvar "LeftShift") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "word_rol") (Var "v2")) (Var "v1")))); Dlet (Pvar "CompUT") (Fun "v1" (App Opapp (App Opapp (Var "word_rol") (App Opapp (App Opapp (Var "word_mul") (Var "v1")) (App Opapp (App Opapp (Var "word_add") (App Opapp (App Opapp (Var "word_add") (Var "v1")) (Var "v1"))) (Let "x" (Val (Lit (IntLit 1))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))))) (Val (Lit (IntLit 5))))); Dlet (Pvar "FwdRound") (Fun "v10" (Fun "v9" (Mat (Var "v10") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v6"; Con "Pair" [App Opapp (App Opapp (Var "word_add") (App Opapp (App Opapp (Var "LeftShift") (App Opapp (App Opapp (Var "word_xor") (Var "v4")) (App Opapp (Var "CompUT") (Var "v3")))) (App Opapp (Var "CompUT") (Var "v6")))) (Var "v1"); Con "Pair" [Var "v3"; App Opapp (App Opapp (Var "word_add") (App Opapp (App Opapp (Var "LeftShift") (App Opapp (App Opapp (Var "word_xor") (Var "v8")) (App Opapp (Var "CompUT") (Var "v6")))) (App Opapp (Var "CompUT") (Var "v3")))) (Var "v2")]]])])])])]))); Dlet (Pvar "BwdRound") (Fun "v10" (Fun "v9" (Mat (Var "v10") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Opapp (App Opapp (Var "word_xor") (App Opapp (App Opapp (Var "RightShift") (App Opapp (App Opapp (Var "word_sub") (Var "v3")) (Var "v2"))) (App Opapp (Var "CompUT") (Var "v4")))) (App Opapp (Var "CompUT") (Var "v8")); Con "Pair" [Var "v8"; Con "Pair" [App Opapp (App Opapp (Var "word_xor") (App Opapp (App Opapp (Var "RightShift") (App Opapp (App Opapp (Var "word_sub") (Var "v6")) (Var "v1"))) (App Opapp (Var "CompUT") (Var "v8")))) (App Opapp (Var "CompUT") (Var "v4")); Var "v4"]]])])])])]))); Dlet (Pvar "PostWhitening") (Fun "v7" (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Opapp (App Opapp (Var "word_add") (Var "v6")) (App Opapp (Var "SND") (App Opapp (Var "GETKEYS") (Var "v7"))); Con "Pair" [Var "v4"; Con "Pair" [App Opapp (App Opapp (Var "word_add") (Var "v2")) (App Opapp (Var "SND") (App Opapp (Var "GETKEYS") (Var "v7"))); Var "v1"]]])])])]))); Dletrec [("Round","v3", Fun "v2" (Fun "v1" (If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (App Opapp (App Opapp (Var "PostWhitening") (Var "v2")) (Var "v1")) (App Opapp (App Opapp (App Opapp (Var "Round") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (App Opapp (Var "ROTKEYS") (Var "v2"))) (App Opapp (App Opapp (Var "FwdRound") (Var "v1")) (App Opapp (Var "GETKEYS") (Var "v2")))))))]; Dletrec [("InvRound","v3", Fun "v2" (Fun "v1" (If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (App Opapp (App Opapp (Var "InvPreWhitening") (Var "v2")) (Var "v1")) (App Opapp (App Opapp (Var "BwdRound") (App Opapp (App Opapp (App Opapp (Var "InvRound") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (App Opapp (Var "ROTKEYS") (Var "v2"))) (Var "v1"))) (App Opapp (Var "GETKEYS") (Var "v2"))))))]; Dlet (Pvar "r") (Val (Lit (IntLit 20))); Dlet (Pvar "RC6_FWD") (Fun "v1" (App Opapp (App Opapp (Var "o") (App Opapp (App Opapp (Var "Round") (Var "r")) (Var "v1"))) (App Opapp (Var "PreWhitening") (Var "v1")))); Dlet (Pvar "RC6_BWD") (Fun "v1" (App Opapp (App Opapp (Var "o") (App Opapp (Var "InvPostWhitening") (Var "v1"))) (App Opapp (App Opapp (Var "InvRound") (Var "r")) (Var "v1"))))]