main = KnuthBendix.Start
KnuthBendix.Start = if (KnuthBendix.checkEquations KnuthBendix.eqns KnuthBendix.sig) (KnuthBendix.emitStr (Flite.str "Using equations:\n") (KnuthBendix.emitStr (KnuthBendix.showEqns KnuthBendix.sig KnuthBendix.eqns) (KnuthBendix.emitStr (KnuthBendix.showResult (KnuthBendix.complete KnuthBendix.sig KnuthBendix.eqns) KnuthBendix.sig) 0))) (KnuthBendix.emitStr (Flite.str "Ill-formed equation\n") 0)
Flite.str !_x_0 = select _x_0 ("" -> Flite.Nil) (_ -> Flite.Cons (Flite.char (string_select _x_0 0)) (Flite.str (<{StdString.%_10}> _x_0 (_Tuple2 1 (string_size _x_0)))))
<{StdString.%_10}> !str_0 !_x_1 = select _x_1 (_Tuple2 a b -> string_slice str_0 a b)
Flite.char !c_0 = toInt_char c_0
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
KnuthBendix.emitStr !_x_0 k_1 = select _x_0 (Flite.Nil -> k_1) (Flite.Cons c_1_0 cs_1_1 -> Flite.emit c_1_0 (KnuthBendix.emitStr cs_1_1 k_1)) 
Flite.emit !c_0 k_1 = StdDebug.trace (<{StdOverloaded.toString;}> toString) (toChar c_0) k_1
:: <{StdOverloaded.toString;}> = {StdOverloaded.toString}
StdDebug.trace !_vtoString_0 !message_1 a_2 = trace (StdOverloaded.get_toString_25 _vtoString_0 message_1) a_2
StdOverloaded.get_toString_25 rec = select rec (<{StdOverloaded.toString;}> a1 -> a1)
KnuthBendix.sig = Flite.Cons (Flite.Pair (Flite.str "+") (Flite.Pair 2 True)) (Flite.Cons (Flite.Pair (Flite.str "-") (Flite.Pair 1 False)) (Flite.Cons (Flite.Pair (Flite.str "0") (Flite.Pair 0 False)) Flite.Nil))
:: Flite.Pair = Flite.Pair a1 a2
KnuthBendix.eqns = Flite.Cons (Flite.Pair (KnuthBendix.fun "+" (Flite.Cons (KnuthBendix.fun "0" Flite.Nil) (Flite.Cons (KnuthBendix.var "X") Flite.Nil))) (KnuthBendix.var "X")) (Flite.Cons (Flite.Pair (KnuthBendix.fun "+" (Flite.Cons (KnuthBendix.fun "-" (Flite.Cons (KnuthBendix.var "X") Flite.Nil)) (Flite.Cons (KnuthBendix.var "X") Flite.Nil))) (KnuthBendix.fun "0" Flite.Nil)) (Flite.Cons (Flite.Pair (KnuthBendix.fun "+" (Flite.Cons (KnuthBendix.fun "+" (Flite.Cons (KnuthBendix.var "X") (Flite.Cons (KnuthBendix.var "Y") Flite.Nil))) (Flite.Cons (KnuthBendix.var "Z") Flite.Nil))) (KnuthBendix.fun "+" (Flite.Cons (KnuthBendix.var "X") (Flite.Cons (KnuthBendix.fun "+" (Flite.Cons (KnuthBendix.var "Y") (Flite.Cons (KnuthBendix.var "Z") Flite.Nil))) Flite.Nil)))) Flite.Nil))
KnuthBendix.var x_0 = KnuthBendix.Var (Flite.str x_0)
:: KnuthBendix.E = KnuthBendix.Fun a1 a2 | KnuthBendix.Var a1
KnuthBendix.fun x_0 y_1 = KnuthBendix.Fun (Flite.str x_0) y_1
KnuthBendix.complete sig_0 !trs_1 = KnuthBendix.completionLoop KnuthBendix.variables 0 trs_1 Flite.Nil
KnuthBendix.variables = let variety_1_0 = Flite.Cons Flite.Nil (KnuthBendix.concatMap KnuthBendix.variations variety_1_0) in KnuthBendix.tail variety_1_0
KnuthBendix.tail !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> xs_1_1) 
KnuthBendix.variations v_0 = KnuthBendix.map (KnuthBendix.flip Flite.Cons v_0) (Flite.str "ABCDEFGHIJKLMNOPQRSTUVWXYZ")
KnuthBendix.flip !f_0 x_1 y_2 = f_0 y_2 x_1
KnuthBendix.map f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons (f_0 x_1_0) (KnuthBendix.map f_0 xs_1_1)) 
KnuthBendix.concatMap f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> KnuthBendix.append (f_0 x_1_0) (KnuthBendix.concatMap f_0 xs_1_1)) 
KnuthBendix.append !_x_0 ys_1 = select _x_0 (Flite.Nil -> ys_1) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons x_1_0 (KnuthBendix.append xs_1_1 ys_1)) 
KnuthBendix.completionLoop vs_0 n_1 !_x_2 rules_3 = select _x_2 (Flite.Nil -> Flite.Just rules_3) (Flite.Cons _x_1_0 rest_1_1 -> select _x_1_0 (Flite.Pair l_2_0 r_2_1 -> <{KnuthBendix._c;230;3_157}> (eq n_1 1000) vs_0 l_2_0 r_2_1 n_1 rest_1_1 rules_3) ) 
<{KnuthBendix._c;230;3_157}> !_x_0 vs_1 l_2 r_3 n_4 rest_5 rules_6 = select _x_0 (True -> Flite.Nothing) (False -> <{KnuthBendix._c;232;12_156}> (KnuthBendix.renameNew vs_1 (Flite.Pair l_2 r_3)) n_4 rest_5 rules_6) 
KnuthBendix.renameNew !vs_0 !_x_1 = select _x_1 (Flite.Pair l_1_0 r_1_1 -> <{KnuthBendix._c;213;3_145}> (KnuthBendix.zipWithRemRight (KnuthBendix.curry (KnuthBendix.cross KnuthBendix.id KnuthBendix.Var)) (KnuthBendix.vars l_1_0) vs_0) l_1_0 r_1_1) 
KnuthBendix.vars !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> Flite.Cons v_1_0 Flite.Nil) (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.foldr (KnuthBendix.unionBy KnuthBendix.equalStrings_133) Flite.Nil (KnuthBendix.map KnuthBendix.vars ts_1_1)) 
KnuthBendix.equalStrings_133 !_x_0 !_x_1 = select _x_0 (Flite.Nil -> select _x_1 (Flite.Nil -> True) (Flite.Cons y_2_0 ys_2_1 -> False) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_1 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> KnuthBendix.con (eq x_1_0 y_2_0) (KnuthBendix.equalStrings_133 xs_1_1 ys_2_1)) ) 
KnuthBendix.con !_x_0 q_1 = if _x_0 q_1 False
KnuthBendix.unionBy e_0 !xs_1 !ys_2 = KnuthBendix.foldr (KnuthBendix.insBy e_0) xs_1 ys_2
KnuthBendix.insBy e_0 x_1 !ys_2 = if (KnuthBendix.elemBy e_0 x_1 ys_2) ys_2 (Flite.Cons x_1 ys_2)
KnuthBendix.elemBy e_0 x_1 !_x_2 = select _x_2 (Flite.Nil -> False) (Flite.Cons y_1_0 ys_1_1 -> if (e_0 x_1 y_1_0) True (KnuthBendix.elemBy e_0 x_1 ys_1_1)) 
KnuthBendix.foldr f_0 z_1 !_x_2 = select _x_2 (Flite.Nil -> z_1) (Flite.Cons x_1_0 xs_1_1 -> f_0 x_1_0 (KnuthBendix.foldr f_0 z_1 xs_1_1)) 
KnuthBendix.id !x_0 = x_0
KnuthBendix.cross f_0 g_1 !_x_2 = select _x_2 (Flite.Pair x_1_0 y_1_1 -> Flite.Pair (f_0 x_1_0) (g_1 y_1_1)) 
KnuthBendix.curry !f_0 x_1 y_2 = f_0 (Flite.Pair x_1 y_2)
KnuthBendix.zipWithRemRight f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> Flite.Pair Flite.Nil Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Pair Flite.Nil (Flite.Cons y_2_0 ys_2_1)) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> Flite.Pair Flite.Nil Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> <{KnuthBendix._c;208;3_144}> (KnuthBendix.zipWithRemRight f_0 xs_1_1 ys_2_1) f_0 x_1_0 y_2_0) ) 
<{KnuthBendix._c;208;3_144}> !_x_0 f_1 x_2 y_3 = select _x_0 (Flite.Pair rest_1_0 rem_1_1 -> Flite.Pair (Flite.Cons (f_1 x_2 y_3) rest_1_0) rem_1_1) 
<{KnuthBendix._c;213;3_145}> !_x_0 l_1 r_2 = select _x_0 (Flite.Pair sub_1_0 rest_1_1 -> Flite.Pair (Flite.Pair (KnuthBendix.subst sub_1_0 l_1) (KnuthBendix.subst sub_1_0 r_2)) rest_1_1) 
KnuthBendix.subst s_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> <{KnuthBendix._c;501;24_141}> s_0 v_1_0) (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.Fun f_1_0 (KnuthBendix.map (KnuthBendix.subst s_0) ts_1_1)) 
<{KnuthBendix._c;501;24_141}> !s_0 v_1 = select s_0 (Flite.Nil -> KnuthBendix.Var v_1) (Flite.Cons _x_1_0 rest_1_1 -> select _x_1_0 (Flite.Pair w_2_0 t_2_1 -> if (KnuthBendix.equalStrings_133 v_1 w_2_0) t_2_1 (KnuthBendix.subst rest_1_1 (KnuthBendix.Var v_1))) ) 
<{KnuthBendix._c;232;12_156}> !_x_0 n_1 rest_2 rules_3 = select _x_0 (Flite.Pair newEqn_1_0 ws_1_1 -> <{KnuthBendix._c;233;30_155}> (KnuthBendix.orient newEqn_1_0) ws_1_1 n_1 rest_2 rules_3) 
KnuthBendix.orient !_x_0 = select _x_0 (Flite.Pair t1_1_0 t2_1_1 -> if (KnuthBendix.order t1_1_0 t2_1_1) (Flite.Just (Flite.Pair t1_1_0 t2_1_1)) (if (KnuthBendix.order t2_1_1 t1_1_0) (Flite.Just (Flite.Pair t2_1_1 t1_1_0)) Flite.Nothing)) 
:: Flite.Maybe = Flite.Nothing | Flite.Just a1
KnuthBendix.order = KnuthBendix.kbGreaterThan KnuthBendix.weights
KnuthBendix.weights = KnuthBendix.Weights 1 (Flite.Cons (Flite.Pair (Flite.str "0") 1) (Flite.Cons (Flite.Pair (Flite.str "+") 0) (Flite.Cons (Flite.Pair (Flite.str "-") 0) Flite.Nil)))
:: KnuthBendix.Weights = KnuthBendix.Weights a1 a2
KnuthBendix.kbGreaterThan !w_0 !t_1 !s_2 = let wt_1_0 = KnuthBendix.termWeight w_0 t_1, ws_1_1 = KnuthBendix.termWeight w_0 s_2, vs_1_2 = KnuthBendix.unionBy KnuthBendix.equalStrings_133 (KnuthBendix.vars t_1) (KnuthBendix.vars s_2), ns_1_3 = KnuthBendix.map KnuthBendix.snd (KnuthBendix.varCounts s_2 vs_1_2), nt_1_4 = KnuthBendix.map KnuthBendix.snd (KnuthBendix.varCounts t_1 vs_1_2) in KnuthBendix.dis (KnuthBendix.con (KnuthBendix.inv (<{KnuthBendix.<=_137}> wt_1_0 ws_1_1)) (KnuthBendix.compareAll <{KnuthBendix.<=_138}> ns_1_3 nt_1_4)) (KnuthBendix.con (KnuthBendix.con (eq wt_1_0 ws_1_1) (KnuthBendix.compareAll eq nt_1_4 ns_1_3)) (KnuthBendix.dis (KnuthBendix.powerOf (KnuthBendix.last (KnuthBendix.funSequence w_0)) t_1 s_2) (KnuthBendix.funcAfter w_0 t_1 s_2)))
KnuthBendix.funcAfter w_0 !_x_1 !_x_2 = select _x_1 (KnuthBendix.Var v_1_0 -> select _x_2 (KnuthBendix.Var x_2_0 -> False) (KnuthBendix.Fun g_2_0 us_2_1 -> False) ) (KnuthBendix.Fun f_1_0 ts_1_1 -> select _x_2 (KnuthBendix.Var x_2_0 -> False) (KnuthBendix.Fun g_2_0 us_2_1 -> if (KnuthBendix.equalStrings_133 f_1_0 g_2_0) (KnuthBendix.orderLex (KnuthBendix.kbGreaterThan w_0) ts_1_1 us_2_1) (KnuthBendix.before_139 (KnuthBendix.funSequence w_0) g_2_0 f_1_0)) ) 
KnuthBendix.funSequence !_x_0 = select _x_0 (KnuthBendix.Weights vw_1_0 fws_1_1 -> KnuthBendix.map KnuthBendix.fst fws_1_1) 
KnuthBendix.fst !_x_0 = select _x_0 (Flite.Pair x_1_0 y_1_1 -> x_1_0) 
KnuthBendix.before_139 !_x_0 !x_1 y_2 = select _x_0 (Flite.Cons h_1_0 t_1_1 -> KnuthBendix.dis (KnuthBendix.equalStrings_133 h_1_0 x_1) (KnuthBendix.con (KnuthBendix.inv (KnuthBendix.equalStrings_133 h_1_0 y_2)) (KnuthBendix.before_139 t_1_1 x_1 y_2))) 
KnuthBendix.inv !_x_0 = if _x_0 False True
KnuthBendix.dis !_x_0 q_1 = if _x_0 True q_1
KnuthBendix.orderLex f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> False) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> if (KnuthBendix.equalTerms x_1_0 y_2_0) (KnuthBendix.orderLex f_0 xs_1_1 ys_2_1) (f_0 x_1_0 y_2_0)) ) 
KnuthBendix.equalTerms !_x_0 !_x_1 = select _x_0 (KnuthBendix.Var v_1_0 -> select _x_1 (KnuthBendix.Var w_2_0 -> KnuthBendix.equalStrings_133 v_1_0 w_2_0) (KnuthBendix.Fun g_2_0 us_2_1 -> False) ) (KnuthBendix.Fun f_1_0 ts_1_1 -> select _x_1 (KnuthBendix.Var w_2_0 -> False) (KnuthBendix.Fun g_2_0 us_2_1 -> KnuthBendix.con (KnuthBendix.equalStrings_133 f_1_0 g_2_0) (KnuthBendix.and (KnuthBendix.zipWith KnuthBendix.equalTerms ts_1_1 us_2_1))) ) 
KnuthBendix.zipWith f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Nil) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Cons (f_0 x_1_0 y_2_0) (KnuthBendix.zipWith f_0 xs_1_1 ys_2_1)) ) 
KnuthBendix.and !xs_0 = KnuthBendix.foldr KnuthBendix.con True xs_0
KnuthBendix.last !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> if (KnuthBendix.null xs_1_1) x_1_0 (KnuthBendix.last xs_1_1)) 
KnuthBendix.null !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False) 
KnuthBendix.powerOf fn_0 !_x_1 u_2 = select _x_1 (KnuthBendix.Var v_1_0 -> False) (KnuthBendix.Fun f_1_0 _x_1_1 -> select _x_1_1 (Flite.Nil -> False) (Flite.Cons x_2_0 xs_2_1 -> KnuthBendix.con (KnuthBendix.con (KnuthBendix.isVar u_2) (KnuthBendix.equalStrings_133 f_1_0 fn_0)) (KnuthBendix.con (KnuthBendix.null xs_2_1) (KnuthBendix.pow fn_0 x_2_0))) ) 
KnuthBendix.pow fn_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> True) (KnuthBendix.Fun f_1_0 _x_1_1 -> select _x_1_1 (Flite.Cons z_2_0 zs_2_1 -> KnuthBendix.con (KnuthBendix.equalStrings_133 f_1_0 fn_0) (KnuthBendix.con (KnuthBendix.null zs_2_1) (KnuthBendix.pow fn_0 z_2_0))) ) 
KnuthBendix.isVar !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> True) (KnuthBendix.Fun f_1_0 ts_1_1 -> False) 
KnuthBendix.compareAll f_0 !xs_1 !ys_2 = KnuthBendix.and (KnuthBendix.zipWith f_0 xs_1 ys_2)
<{KnuthBendix.<=_138}> !x_0 !y_1 = not (lt y_1 x_0)
<{KnuthBendix.<=_137}> !x_0 !y_1 = not (lt y_1 x_0)
KnuthBendix.varCounts !t_0 !vs_1 = KnuthBendix.foldr KnuthBendix.tally_136 (KnuthBendix.zip vs_1 (KnuthBendix.repeat 0)) (KnuthBendix.concatMap (KnuthBendix.varAt t_0) (KnuthBendix.positions t_0))
KnuthBendix.positions !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> Flite.Cons Flite.Nil Flite.Nil) (KnuthBendix.Fun f_1_0 ts_1_1 -> Flite.Cons Flite.Nil (KnuthBendix.concatMap (KnuthBendix.argPositions ts_1_1) (KnuthBendix.enumFromTo 1 (KnuthBendix.len ts_1_1)))) 
KnuthBendix.len !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> KnuthBendix.incr (KnuthBendix.len xs_1_1)) 
KnuthBendix.incr !i_0 = add i_0 1
KnuthBendix.enumFromTo !m_0 !n_1 = if (<{KnuthBendix.<=_131}> m_0 n_1) (Flite.Cons m_0 (KnuthBendix.enumFromTo (KnuthBendix.incr m_0) n_1)) Flite.Nil
<{KnuthBendix.<=_131}> !x_0 !y_1 = not (lt y_1 x_0)
KnuthBendix.argPositions !ts_0 !n_1 = KnuthBendix.map (Flite.Cons n_1) (KnuthBendix.positions (KnuthBendix.elemAt ts_0 (KnuthBendix.decr n_1)))
KnuthBendix.decr !i_0 = sub i_0 1
KnuthBendix.elemAt !_x_0 !n_1 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> if (eq n_1 0) x_1_0 (KnuthBendix.elemAt xs_1_1 (KnuthBendix.decr n_1))) 
KnuthBendix.varAt !t_0 !p_1 = <{KnuthBendix._c;365;15_143}> (KnuthBendix.subterm t_0 p_1)
KnuthBendix.subterm !t_0 !_x_1 = select _x_1 (Flite.Nil -> t_0) (Flite.Cons p1_1_0 pRest_1_1 -> <{KnuthBendix._c;524;31_142}> t_0 p1_1_0 pRest_1_1) 
<{KnuthBendix._c;524;31_142}> !t_0 !p1_1 !pRest_2 = select t_0 (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.subterm (KnuthBendix.elemAt ts_1_1 (KnuthBendix.decr p1_1)) pRest_2) 
<{KnuthBendix._c;365;15_143}> !_x_0 = select _x_0 (KnuthBendix.Var v_1_0 -> Flite.Cons v_1_0 Flite.Nil) (KnuthBendix.Fun f_1_0 ts_1_1 -> Flite.Nil) 
KnuthBendix.repeat x_0 = Flite.Cons x_0 (KnuthBendix.repeat x_0)
KnuthBendix.zip = KnuthBendix.zipWith Flite.Pair
KnuthBendix.tally_136 k_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons _x_1_0 xs_1_1 -> select _x_1_0 (Flite.Pair x_2_0 nx_2_1 -> if (KnuthBendix.equalStrings_133 k_0 x_2_0) (Flite.Cons (Flite.Pair x_2_0 (KnuthBendix.incr nx_2_1)) xs_1_1) (Flite.Cons (Flite.Pair x_2_0 nx_2_1) (KnuthBendix.tally_136 k_0 xs_1_1))) ) 
KnuthBendix.snd !_x_0 = select _x_0 (Flite.Pair x_1_0 y_1_1 -> y_1_1) 
KnuthBendix.termWeight !w_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> KnuthBendix.varWeight w_0) (KnuthBendix.Fun f_1_0 ts_1_1 -> add (KnuthBendix.funWeight_135 w_0 f_1_0) (KnuthBendix.sum (KnuthBendix.map (KnuthBendix.termWeight w_0) ts_1_1))) 
KnuthBendix.sum !xs_0 = KnuthBendix.foldr KnuthBendix.plus_132 0 xs_0
KnuthBendix.plus_132 !a_0 !b_1 = add a_0 b_1
KnuthBendix.funWeight_135 !_x_0 !f_1 = select _x_0 (KnuthBendix.Weights vw_1_0 fws_1_1 -> KnuthBendix.fromJust (KnuthBendix.lookUpBy KnuthBendix.equalStrings_133 f_1 fws_1_1)) 
KnuthBendix.lookUpBy e_0 x_1 !_x_2 = select _x_2 (Flite.Nil -> Flite.Nothing) (Flite.Cons _x_1_0 yvs_1_1 -> select _x_1_0 (Flite.Pair y_2_0 v_2_1 -> if (e_0 x_1 y_2_0) (Flite.Just v_2_1) (KnuthBendix.lookUpBy e_0 x_1 yvs_1_1)) ) 
KnuthBendix.fromJust !_x_0 = select _x_0 (Flite.Just x_1_0 -> x_1_0) 
KnuthBendix.varWeight !_x_0 = select _x_0 (KnuthBendix.Weights vw_1_0 fws_1_1 -> vw_1_0) 
<{KnuthBendix._c;233;30_155}> !_x_0 ws_1 n_2 rest_3 rules_4 = select _x_0 (Flite.Nothing -> Flite.Nothing) (Flite.Just newRule_1_0 -> KnuthBendix.completionWith ws_1 (KnuthBendix.incr n_2) rest_3 newRule_1_0 rules_4) 
KnuthBendix.completionWith vs_0 n_1 !rest_2 newRule_3 !rules_4 = <{KnuthBendix._c;242;7_158}> (KnuthBendix.simplifyRules KnuthBendix.sig newRule_3 rules_4) vs_0 n_1 newRule_3 rules_4 rest_2
KnuthBendix.simplifyRules sig_0 rule_1 !trs_2 = <{KnuthBendix._c;262;3_150}> (KnuthBendix.reduceSplit sig_0 rule_1 trs_2) rule_1
KnuthBendix.reduceSplit sig_0 rule_1 !_x_2 = select _x_2 (Flite.Nil -> Flite.Pair Flite.Nil Flite.Nil) (Flite.Cons _x_1_0 rs_1_1 -> select _x_1_0 (Flite.Pair l_2_0 r_2_1 -> <{KnuthBendix._c;280;3_149}> (KnuthBendix.reduceSplit sig_0 rule_1 rs_1_1) rule_1 l_2_0 r_2_1) ) 
<{KnuthBendix._c;280;3_149}> !_x_0 rule_1 !l_2 r_3 = select _x_0 (Flite.Pair eqns_1_0 rules_1_1 -> let reducedl_2_0 = KnuthBendix.reduce (Flite.Cons rule_1 Flite.Nil) l_2 in if (KnuthBendix.dis (KnuthBendix.null reducedl_2_0) (KnuthBendix.reducible (Flite.Cons (Flite.Pair l_2 r_3) Flite.Nil) (KnuthBendix.left rule_1))) (Flite.Pair eqns_1_0 (Flite.Cons (Flite.Pair l_2 r_3) rules_1_1)) (Flite.Pair (Flite.Cons (Flite.Pair (KnuthBendix.head reducedl_2_0) r_3) eqns_1_0) rules_1_1)) 
KnuthBendix.head !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> x_1_0) 
KnuthBendix.left = KnuthBendix.fst
KnuthBendix.reducible trs_0 !t_1 = KnuthBendix.inv (KnuthBendix.null (KnuthBendix.reduce trs_0 t_1))
KnuthBendix.reduce trs_0 !t_1 = KnuthBendix.concatMap (KnuthBendix.reduceAt trs_0 t_1) (KnuthBendix.positions t_1)
KnuthBendix.reduceAt trs_0 !t_1 !p_2 = if (KnuthBendix.isVar (KnuthBendix.subterm t_1 p_2)) Flite.Nil (KnuthBendix.concatMap (KnuthBendix.reduceAtWith t_1 p_2) trs_0)
KnuthBendix.reduceAtWith t_0 p_1 !_x_2 = select _x_2 (Flite.Pair l_1_0 r_1_1 -> <{KnuthBendix._c;493;3_148}> (KnuthBendix.match l_1_0 (KnuthBendix.subterm t_0 p_1)) r_1_1 p_1 t_0) 
KnuthBendix.match !t1_0 t2_1 = KnuthBendix.matchWith (Flite.Cons t1_0 Flite.Nil) (Flite.Cons t2_1 Flite.Nil) Flite.Nil
KnuthBendix.matchWith !_x_0 !_x_1 sub_2 = select _x_0 (Flite.Nil -> select _x_1 (Flite.Nil -> Flite.Just sub_2) ) (Flite.Cons _x_1_0 ts1_1_1 -> select _x_1_0 (KnuthBendix.Var v_2_0 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> if (KnuthBendix.elemBy KnuthBendix.equalStrings_133 v_2_0 (KnuthBendix.map KnuthBendix.fst sub_2)) (if (KnuthBendix.equalTerms t_3_0 (KnuthBendix.subst sub_2 (KnuthBendix.Var v_2_0))) (KnuthBendix.matchWith ts1_1_1 ts2_3_1 sub_2) Flite.Nothing) (KnuthBendix.matchWith ts1_1_1 ts2_3_1 (Flite.Cons (Flite.Pair v_2_0 t_3_0) sub_2))) ) (KnuthBendix.Fun f_2_0 ts_2_1 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> <{KnuthBendix._c;465;3_146}> t_3_0 f_2_0 ts_2_1 ts1_1_1 ts2_3_1 sub_2) ) ) 
<{KnuthBendix._c;465;3_146}> !t_0 f_1 ts_2 ts1_3 ts2_4 sub_5 = select t_0 (KnuthBendix.Var v_1_0 -> Flite.Nothing) (KnuthBendix.Fun g_1_0 us_1_1 -> if (KnuthBendix.equalStrings_133 f_1 g_1_0) (KnuthBendix.matchWith (KnuthBendix.append ts_2 ts1_3) (KnuthBendix.append us_1_1 ts2_4) sub_5) Flite.Nothing) 
<{KnuthBendix._c;493;3_148}> !_x_0 r_1 p_2 t_3 = select _x_0 (Flite.Nothing -> Flite.Nil) (Flite.Just sub_1_0 -> Flite.Cons (KnuthBendix.placeAt (KnuthBendix.subst sub_1_0 r_1) p_2 t_3) Flite.Nil) 
KnuthBendix.placeAt t_0 !_x_1 u_2 = select _x_1 (Flite.Nil -> t_0) (Flite.Cons p_1_0 pRest_1_1 -> <{KnuthBendix._c;529;32_147}> u_2 t_0 pRest_1_1 p_1_0) 
<{KnuthBendix._c;529;32_147}> !u_0 t_1 pRest_2 p_3 = select u_0 (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.Fun f_1_0 (KnuthBendix.applyToIndex (KnuthBendix.placeAt t_1 pRest_2) (KnuthBendix.decr p_3) ts_1_1)) 
KnuthBendix.applyToIndex f_0 !n_1 !_x_2 = select _x_2 (Flite.Cons x_1_0 xs_1_1 -> if (eq n_1 0) (Flite.Cons (f_0 x_1_0) xs_1_1) (Flite.Cons x_1_0 (KnuthBendix.applyToIndex f_0 (KnuthBendix.decr n_1) xs_1_1))) 
<{KnuthBendix._c;262;3_150}> !_x_0 rule_1 = select _x_0 (Flite.Pair newEqns_1_0 remainingRules_1_1 -> Flite.Pair newEqns_1_0 (KnuthBendix.uniqueRules (KnuthBendix.map (KnuthBendix.normRhs (Flite.Cons rule_1 remainingRules_1_1)) (Flite.Cons rule_1 remainingRules_1_1)))) 
KnuthBendix.normRhs trs_0 !_x_1 = select _x_1 (Flite.Pair l_1_0 r_1_1 -> Flite.Pair l_1_0 (KnuthBendix.norm trs_0 r_1_1)) 
KnuthBendix.norm trs_0 !t_1 = KnuthBendix.head (KnuthBendix.normalForms trs_0 t_1)
KnuthBendix.normalForms trs_0 !t_1 = let reduced_1_0 = KnuthBendix.reduce trs_0 t_1 in if (KnuthBendix.null reduced_1_0) (Flite.Cons t_1 Flite.Nil) (KnuthBendix.concatMap (KnuthBendix.normalForms trs_0) reduced_1_0)
KnuthBendix.uniqueRules = KnuthBendix.nubBy KnuthBendix.equivPair
KnuthBendix.equivPair !_x_0 !_x_1 = select _x_0 (Flite.Pair a_1_0 b_1_1 -> select _x_1 (Flite.Pair c_2_0 d_2_1 -> KnuthBendix.dis (KnuthBendix.con (KnuthBendix.equiv a_1_0 c_2_0) (KnuthBendix.equiv b_1_1 d_2_1)) (KnuthBendix.con (KnuthBendix.equiv a_1_0 d_2_1) (KnuthBendix.equiv b_1_1 c_2_0))) ) 
KnuthBendix.equiv !t_0 !u_1 = KnuthBendix.con (KnuthBendix.isJust (KnuthBendix.match t_0 u_1)) (KnuthBendix.isJust (KnuthBendix.match u_1 t_0))
KnuthBendix.isJust !_x_0 = select _x_0 (Flite.Nothing -> False) (Flite.Just x_1_0 -> True) 
KnuthBendix.nubBy e_0 !xs_1 = KnuthBendix.nubBySans Flite.Nil e_0 xs_1
KnuthBendix.nubBySans ss_0 e_1 !_x_2 = select _x_2 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> if (KnuthBendix.elemBy e_1 x_1_0 ss_0) (KnuthBendix.nubBySans ss_0 e_1 xs_1_1) (Flite.Cons x_1_0 (KnuthBendix.nubBySans (Flite.Cons x_1_0 ss_0) e_1 xs_1_1))) 
<{KnuthBendix._c;242;7_158}> !_x_0 vs_1 n_2 newRule_3 rules_4 !rest_5 = select _x_0 (Flite.Pair eqs_1_0 rls_1_1 -> KnuthBendix.completionLoop vs_1 n_2 (KnuthBendix.simplifyEquations KnuthBendix.sig (Flite.Cons newRule_3 rules_4) (KnuthBendix.append rest_5 (KnuthBendix.append eqs_1_0 (KnuthBendix.getCriticalPairs (Flite.Cons newRule_3 rules_4) newRule_3)))) (KnuthBendix.uniqueRules rls_1_1)) 
KnuthBendix.getCriticalPairs trs_0 !r_1 = KnuthBendix.append (KnuthBendix.selfCriticalPairs trs_0 r_1) (KnuthBendix.concatMap (KnuthBendix.duoCriticalPairs trs_0 r_1) trs_0)
KnuthBendix.duoCriticalPairs trs_0 !_x_1 !_x_2 = select _x_1 (Flite.Pair l1_1_0 r1_1_1 -> select _x_2 (Flite.Pair l2_2_0 r2_2_1 -> KnuthBendix.append (KnuthBendix.criticalPairs trs_0 True (Flite.Pair l1_1_0 r1_1_1) (Flite.Pair l2_2_0 r2_2_1)) (KnuthBendix.criticalPairs trs_0 False (Flite.Pair l2_2_0 r2_2_1) (Flite.Pair l1_1_0 r1_1_1))) ) 
KnuthBendix.criticalPairs trs_0 !allowRootPos_1 !_x_2 !_x_3 = select _x_2 (Flite.Pair l1_1_0 r1_1_1 -> select _x_3 (Flite.Pair l2_2_0 r2_2_1 -> KnuthBendix.concatMap (KnuthBendix.criticalPairsAt trs_0 (Flite.Pair l1_1_0 r1_1_1) (Flite.Pair l2_2_0 r2_2_1)) (<{KnuthBendix._c;299;14_154}> allowRootPos_1 l1_1_0)) ) 
<{KnuthBendix._c;299;14_154}> !allowRootPos_0 !l1_1 = select allowRootPos_0 (True -> KnuthBendix.positions l1_1) (False -> KnuthBendix.filter (KnuthBendix.non KnuthBendix.null) (KnuthBendix.positions l1_1)) 
KnuthBendix.non !f_0 x_1 = KnuthBendix.inv (f_0 x_1)
KnuthBendix.filter p_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> if (p_0 x_1_0) (Flite.Cons x_1_0 (KnuthBendix.filter p_0 xs_1_1)) (KnuthBendix.filter p_0 xs_1_1)) 
KnuthBendix.criticalPairsAt trs_0 !_x_1 !_x_2 !p_3 = select _x_1 (Flite.Pair l1_1_0 r1_1_1 -> select _x_2 (Flite.Pair l2_2_0 r2_2_1 -> let t_3_0 = KnuthBendix.subterm l1_1_0 p_3 in <{KnuthBendix._c;308;7_153}> (KnuthBendix.isVar t_3_0) t_3_0 l2_2_0 trs_0 r1_1_1 r2_2_1 p_3 l1_1_0) ) 
<{KnuthBendix._c;308;7_153}> !_x_0 t_1 l2_2 trs_3 r1_4 r2_5 p_6 l1_7 = select _x_0 (True -> Flite.Nil) (False -> <{KnuthBendix._c;310;16_152}> (KnuthBendix.unify t_1 l2_2) trs_3 r1_4 r2_5 p_6 l1_7) 
KnuthBendix.unify !t1_0 !t2_1 = KnuthBendix.unifyWith (Flite.Cons t1_0 Flite.Nil) (Flite.Cons t2_1 Flite.Nil) Flite.Nil
KnuthBendix.unifyWith !_x_0 !_x_1 sub_2 = select _x_0 (Flite.Nil -> select _x_1 (Flite.Nil -> Flite.Just sub_2) ) (Flite.Cons _x_1_0 ts1_1_1 -> select _x_1_0 (KnuthBendix.Var v_2_0 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> if (KnuthBendix.equalTerms t_3_0 (KnuthBendix.Var v_2_0)) (KnuthBendix.unifyWith ts1_1_1 ts2_3_1 sub_2) (let vi_4_0 = KnuthBendix.subst sub_2 (KnuthBendix.Var v_2_0) in if (KnuthBendix.equalTerms vi_4_0 (KnuthBendix.Var v_2_0)) (let ti_5_0 = KnuthBendix.subst sub_2 t_3_0 in if (KnuthBendix.elemBy KnuthBendix.equalStrings_133 v_2_0 (KnuthBendix.vars ti_5_0)) Flite.Nothing (KnuthBendix.unifyWith ts1_1_1 ts2_3_1 (KnuthBendix.substAdd (Flite.Cons (Flite.Pair v_2_0 ti_5_0) Flite.Nil) sub_2))) (let ti_5_0 = KnuthBendix.subst sub_2 t_3_0, mgu_5_1 = KnuthBendix.unify vi_4_0 ti_5_0 in if (KnuthBendix.isJust mgu_5_1) (KnuthBendix.unifyWith ts1_1_1 ts2_3_1 (KnuthBendix.substAdd (KnuthBendix.fromJust mgu_5_1) sub_2)) Flite.Nothing))) ) (KnuthBendix.Fun f_2_0 ts_2_1 -> select _x_1 (Flite.Cons t_3_0 ts2_3_1 -> <{KnuthBendix._c;443;3_151}> t_3_0 ts2_3_1 f_2_0 ts_2_1 ts1_1_1 sub_2) ) ) 
<{KnuthBendix._c;443;3_151}> !t_0 ts2_1 f_2 ts_3 ts1_4 sub_5 = select t_0 (KnuthBendix.Var v_1_0 -> KnuthBendix.unifyWith (Flite.Cons (KnuthBendix.Var v_1_0) ts2_1) (Flite.Cons (KnuthBendix.Fun f_2 ts_3) ts1_4) sub_5) (KnuthBendix.Fun g_1_0 us_1_1 -> if (KnuthBendix.equalStrings_133 f_2 g_1_0) (KnuthBendix.unifyWith (KnuthBendix.append ts_3 ts1_4) (KnuthBendix.append us_1_1 ts2_1) sub_5) Flite.Nothing) 
KnuthBendix.substAdd !subNew_0 subOld_1 = KnuthBendix.append subNew_0 (KnuthBendix.map (KnuthBendix.cross KnuthBendix.id (KnuthBendix.subst subNew_0)) subOld_1)
<{KnuthBendix._c;310;16_152}> !_x_0 trs_1 r1_2 r2_3 p_4 l1_5 = select _x_0 (Flite.Nothing -> Flite.Nil) (Flite.Just sub_1_0 -> KnuthBendix.criticalPairsFrom (KnuthBendix.norm trs_1 (KnuthBendix.subst sub_1_0 r1_2)) (KnuthBendix.norm trs_1 (KnuthBendix.placeAt (KnuthBendix.subst sub_1_0 r2_3) p_4 (KnuthBendix.subst sub_1_0 l1_5)))) 
KnuthBendix.criticalPairsFrom !cpl_0 !cpr_1 = if (KnuthBendix.equalTerms cpl_0 cpr_1) Flite.Nil (Flite.Cons (Flite.Pair cpl_0 cpr_1) Flite.Nil)
KnuthBendix.selfCriticalPairs trs_0 !_x_1 = select _x_1 (Flite.Pair l1_1_0 r1_1_1 -> KnuthBendix.criticalPairs trs_0 False (Flite.Pair l1_1_0 r1_1_1) (KnuthBendix.rename (Flite.Pair l1_1_0 r1_1_1))) 
KnuthBendix.rename !_x_0 = select _x_0 (Flite.Pair l_1_0 r_1_1 -> let oldVars_2_0 = KnuthBendix.vars l_1_0, sub_2_1 = KnuthBendix.zip oldVars_2_0 (KnuthBendix.map KnuthBendix.Var (KnuthBendix.filter (KnuthBendix.non (KnuthBendix.flip (KnuthBendix.elemBy KnuthBendix.equalStrings_133) oldVars_2_0)) KnuthBendix.variables)) in Flite.Pair (KnuthBendix.subst sub_2_1 l_1_0) (KnuthBendix.subst sub_2_1 r_1_1)) 
KnuthBendix.simplifyEquations sig_0 trs_1 !eqns_2 = KnuthBendix.filter (KnuthBendix.non (KnuthBendix.uncurry KnuthBendix.equalTerms)) (KnuthBendix.uniqueRules (KnuthBendix.map (KnuthBendix.normEqn trs_1) eqns_2))
KnuthBendix.normEqn trs_0 !_x_1 = select _x_1 (Flite.Pair l_1_0 r_1_1 -> Flite.Pair (KnuthBendix.norm trs_0 l_1_0) (KnuthBendix.norm trs_0 r_1_1)) 
KnuthBendix.uncurry !f_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> f_0 x_1_0 y_1_1) 
KnuthBendix.showResult !_x_0 sig_1 = select _x_0 (Flite.Just trs_1_0 -> KnuthBendix.append (Flite.str "\nSuccess\n") (KnuthBendix.showRules sig_1 (KnuthBendix.map KnuthBendix.rn trs_1_0))) (Flite.Nothing -> Flite.str "\nFailure\n") 
KnuthBendix.rn !_x_0 = select _x_0 (Flite.Pair l_1_0 r_1_1 -> let sub_2_0 = KnuthBendix.zip (KnuthBendix.vars l_1_0) (KnuthBendix.map KnuthBendix.Var KnuthBendix.variables) in Flite.Pair (KnuthBendix.subst sub_2_0 l_1_0) (KnuthBendix.subst sub_2_0 r_1_1)) 
KnuthBendix.showRules sig_0 !rules_1 = KnuthBendix.unlines (KnuthBendix.map (KnuthBendix.showRule sig_0) rules_1)
KnuthBendix.showRule sig_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> KnuthBendix.append (KnuthBendix.showTerm sig_0 x_1_0) (KnuthBendix.append (Flite.str " -> ") (KnuthBendix.showTerm sig_0 y_1_1))) 
KnuthBendix.showTerm sig_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> v_1_0) (KnuthBendix.Fun f_1_0 ts_1_1 -> if (KnuthBendix.isInfix_134 sig_0 f_1_0) (KnuthBendix.append (Flite.str "(") (KnuthBendix.append (KnuthBendix.showTerm sig_0 (KnuthBendix.elemAt ts_1_1 0)) (KnuthBendix.append (Flite.str " ") (KnuthBendix.append f_1_0 (KnuthBendix.append (Flite.str " ") (KnuthBendix.append (KnuthBendix.showTerm sig_0 (KnuthBendix.elemAt ts_1_1 1)) (Flite.str ")"))))))) (if (KnuthBendix.null ts_1_1) f_1_0 (KnuthBendix.append f_1_0 (KnuthBendix.append (Flite.str "(") (KnuthBendix.append (KnuthBendix.concatStrings (KnuthBendix.intersperse (Flite.str ",") (KnuthBendix.map (KnuthBendix.showTerm sig_0) ts_1_1))) (Flite.str ")")))))) 
KnuthBendix.intersperse i_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 _x_1_1 -> select _x_1_1 (Flite.Nil -> Flite.Cons x_1_0 Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Cons x_1_0 (Flite.Cons i_0 (KnuthBendix.intersperse i_0 (Flite.Cons y_2_0 ys_2_1)))) ) 
KnuthBendix.concatStrings !ss_0 = KnuthBendix.foldr KnuthBendix.append Flite.Nil ss_0
KnuthBendix.isInfix_134 !sig_0 f_1 = KnuthBendix.maybe False KnuthBendix.snd (KnuthBendix.lookUpBy KnuthBendix.equalStrings_133 f_1 sig_0)
KnuthBendix.maybe n_0 j_1 !_x_2 = select _x_2 (Flite.Nothing -> n_0) (Flite.Just x_1_0 -> j_1 x_1_0) 
KnuthBendix.unlines !_x_0 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons s_1_0 ss_1_1 -> KnuthBendix.append s_1_0 (Flite.Cons (Flite.char '\n') (KnuthBendix.unlines ss_1_1))) 
KnuthBendix.showEqns sig_0 !eqns_1 = KnuthBendix.unlines (KnuthBendix.map (KnuthBendix.showEqn sig_0) eqns_1)
KnuthBendix.showEqn sig_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> KnuthBendix.append (KnuthBendix.showTerm sig_0 x_1_0) (KnuthBendix.append (Flite.str " = ") (KnuthBendix.showTerm sig_0 y_1_1))) 
KnuthBendix.checkEquations !es_0 sig_1 = KnuthBendix.all (KnuthBendix.both (KnuthBendix.checkTerm sig_1)) es_0
KnuthBendix.checkTerm sig_0 !_x_1 = select _x_1 (KnuthBendix.Var v_1_0 -> True) (KnuthBendix.Fun f_1_0 ts_1_1 -> KnuthBendix.con (eq (KnuthBendix.len ts_1_1) (KnuthBendix.arity_140 sig_0 f_1_0)) (KnuthBendix.all (KnuthBendix.checkTerm sig_0) ts_1_1)) 
KnuthBendix.all p_0 !xs_1 = KnuthBendix.and (KnuthBendix.map p_0 xs_1)
KnuthBendix.arity_140 !sig_0 f_1 = KnuthBendix.maybe (sub 0 1) KnuthBendix.fst (KnuthBendix.lookUpBy KnuthBendix.equalStrings_133 f_1 sig_0)
KnuthBendix.both !p_0 !_x_1 = select _x_1 (Flite.Pair x_1_0 y_1_1 -> KnuthBendix.con (p_0 x_1_0) (p_0 y_1_1))