fmod SUM is sorts MyNat MyList InVec . *** DT definitions (constructors) op 0 : -> MyNat [ctor] . op s : MyNat -> MyNat [ctor] . op [] : -> MyList [ctor] . op cons : MyNat MyList -> MyList [ctor] . *** defined function names (to be induced, preds, bk) op sum : MyList -> MyNat [metadata "induce"] . *** input encapsulation op in : MyList -> InVec [ctor] . eq sum([]) = 0 . eq sum(cons(0,[])) = 0 . eq sum(cons(s(0),[])) = s(0) . eq sum(cons(s(s(0)),[])) = s(s(0)) . eq sum(cons(s(s(s(0))),[])) = s(s(s(0))) . eq sum(cons(0,cons(0,[]))) = 0 . eq sum(cons(0,cons(s(0),[]))) = s(0) . eq sum(cons(0,cons(s(s(0)),[]))) = s(s(0)) . eq sum(cons(0,cons(s(s(s(0))),[]))) = s(s(s(0))) . eq sum(cons(s(0),cons(0,[]))) = s(0) . eq sum(cons(s(0),cons(s(0),[]))) = s(s(0)) . eq sum(cons(s(0),cons(s(s(0)),[]))) = s(s(s(0))) . eq sum(cons(s(0),cons(s(s(s(0))),[]))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(0,[]))) = s(s(0)) . eq sum(cons(s(s(0)),cons(s(0),[]))) = s(s(s(0))) . eq sum(cons(s(s(0)),cons(s(s(0)),[]))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),[]))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(0,[]))) = s(s(s(0))) . eq sum(cons(s(s(s(0))),cons(s(0),[]))) = s(s(s(s(0)))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),[]))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),[]))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(0,cons(0,[])))) = 0 . eq sum(cons(0,cons(0,cons(s(0),[])))) = s(0) . eq sum(cons(0,cons(0,cons(s(s(0)),[])))) = s(s(0)) . eq sum(cons(0,cons(0,cons(s(s(s(0))),[])))) = s(s(s(0))) . eq sum(cons(0,cons(s(0),cons(0,[])))) = s(0) . eq sum(cons(0,cons(s(0),cons(s(0),[])))) = s(s(0)) . eq sum(cons(0,cons(s(0),cons(s(s(0)),[])))) = s(s(s(0))) . eq sum(cons(0,cons(s(0),cons(s(s(s(0))),[])))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(0)),cons(0,[])))) = s(s(0)) . eq sum(cons(0,cons(s(s(0)),cons(s(0),[])))) = s(s(s(0))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(0)),[])))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(s(0))),[])))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(s(0))),cons(0,[])))) = s(s(s(0))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(0),[])))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(0)),[])))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(0,cons(0,[])))) = s(0) . eq sum(cons(s(0),cons(0,cons(s(0),[])))) = s(s(0)) . eq sum(cons(s(0),cons(0,cons(s(s(0)),[])))) = s(s(s(0))) . eq sum(cons(s(0),cons(0,cons(s(s(s(0))),[])))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(0),cons(0,[])))) = s(s(0)) . eq sum(cons(s(0),cons(s(0),cons(s(0),[])))) = s(s(s(0))) . eq sum(cons(s(0),cons(s(0),cons(s(s(0)),[])))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(0),cons(s(s(s(0))),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(0)),cons(0,[])))) = s(s(s(0))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(0),[])))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(0)),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(0,[])))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(0),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(0)),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(0,cons(0,[])))) = s(s(0)) . eq sum(cons(s(s(0)),cons(0,cons(s(0),[])))) = s(s(s(0))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(0)),[])))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(s(0))),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(0),cons(0,[])))) = s(s(s(0))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(0),[])))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(0)),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(0,[])))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(0),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(0,[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(0),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),[])))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(0,cons(0,[])))) = s(s(s(0))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(0),[])))) = s(s(s(s(0)))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(0)),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(s(0))),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(0,[])))) = s(s(s(s(0)))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(0),[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(0)),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(0,[])))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(0),[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),[])))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(0,[])))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),[])))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),[])))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),[])))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(0,cons(0,cons(0,cons(0,[]))))) = 0 . eq sum(cons(0,cons(0,cons(0,cons(s(0),[]))))) = s(0) . eq sum(cons(0,cons(0,cons(0,cons(s(s(0)),[]))))) = s(s(0)) . eq sum(cons(0,cons(0,cons(0,cons(s(s(s(0))),[]))))) = s(s(s(0))) . eq sum(cons(0,cons(0,cons(s(0),cons(0,[]))))) = s(0) . eq sum(cons(0,cons(0,cons(s(0),cons(s(0),[]))))) = s(s(0)) . eq sum(cons(0,cons(0,cons(s(0),cons(s(s(0)),[]))))) = s(s(s(0))) . eq sum(cons(0,cons(0,cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(0,cons(s(s(0)),cons(0,[]))))) = s(s(0)) . eq sum(cons(0,cons(0,cons(s(s(0)),cons(s(0),[]))))) = s(s(s(0))) . eq sum(cons(0,cons(0,cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(0,cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(0,cons(s(s(s(0))),cons(0,[]))))) = s(s(s(0))) . eq sum(cons(0,cons(0,cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(0,cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(0,cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(0),cons(0,cons(0,[]))))) = s(0) . eq sum(cons(0,cons(s(0),cons(0,cons(s(0),[]))))) = s(s(0)) . eq sum(cons(0,cons(s(0),cons(0,cons(s(s(0)),[]))))) = s(s(s(0))) . eq sum(cons(0,cons(s(0),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(0),cons(s(0),cons(0,[]))))) = s(s(0)) . eq sum(cons(0,cons(s(0),cons(s(0),cons(s(0),[]))))) = s(s(s(0))) . eq sum(cons(0,cons(s(0),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(0),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(0),cons(s(s(0)),cons(0,[]))))) = s(s(s(0))) . eq sum(cons(0,cons(s(0),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(0),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(0),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(0),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(0),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(0,cons(s(s(0)),cons(0,cons(0,[]))))) = s(s(0)) . eq sum(cons(0,cons(s(s(0)),cons(0,cons(s(0),[]))))) = s(s(s(0))) . eq sum(cons(0,cons(s(s(0)),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(0)),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(0)),cons(s(0),cons(0,[]))))) = s(s(s(0))) . eq sum(cons(0,cons(s(s(0)),cons(s(0),cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(0)),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(0)),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(0,cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(0,cons(s(s(s(0))),cons(0,cons(0,[]))))) = s(s(s(0))) . eq sum(cons(0,cons(s(s(s(0))),cons(0,cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(s(0))),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(s(0))),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(0),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(0,cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(0),cons(0,cons(0,cons(0,[]))))) = s(0) . eq sum(cons(s(0),cons(0,cons(0,cons(s(0),[]))))) = s(s(0)) . eq sum(cons(s(0),cons(0,cons(0,cons(s(s(0)),[]))))) = s(s(s(0))) . eq sum(cons(s(0),cons(0,cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(0,cons(s(0),cons(0,[]))))) = s(s(0)) . eq sum(cons(s(0),cons(0,cons(s(0),cons(s(0),[]))))) = s(s(s(0))) . eq sum(cons(s(0),cons(0,cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(0,cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(0,cons(s(s(0)),cons(0,[]))))) = s(s(s(0))) . eq sum(cons(s(0),cons(0,cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(0,cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(0,cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(0,cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(0,cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(0,cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(0,cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(0),cons(0,cons(0,[]))))) = s(s(0)) . eq sum(cons(s(0),cons(s(0),cons(0,cons(s(0),[]))))) = s(s(s(0))) . eq sum(cons(s(0),cons(s(0),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(0),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(0),cons(s(0),cons(0,[]))))) = s(s(s(0))) . eq sum(cons(s(0),cons(s(0),cons(s(0),cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(0),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(0),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(0),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(0),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(0),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(0),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(0),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(0),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(0),cons(s(s(0)),cons(0,cons(0,[]))))) = s(s(s(0))) . eq sum(cons(s(0),cons(s(s(0)),cons(0,cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(s(0)),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(0)),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(0),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(0,cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(0,cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(0),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(0)),cons(0,cons(0,cons(0,[]))))) = s(s(0)) . eq sum(cons(s(s(0)),cons(0,cons(0,cons(s(0),[]))))) = s(s(s(0))) . eq sum(cons(s(s(0)),cons(0,cons(0,cons(s(s(0)),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(0,cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(0,cons(s(0),cons(0,[]))))) = s(s(s(0))) . eq sum(cons(s(s(0)),cons(0,cons(s(0),cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(0,cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(0,cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(0)),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(0,cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(0),cons(0,cons(0,[]))))) = s(s(s(0))) . eq sum(cons(s(s(0)),cons(s(0),cons(0,cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(s(0),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(0),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(0),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(0,cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(0,cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(0),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(0,cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(0,cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(0),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(s(0))))))))))) . eq sum(cons(s(s(s(0))),cons(0,cons(0,cons(0,[]))))) = s(s(s(0))) . eq sum(cons(s(s(s(0))),cons(0,cons(0,cons(s(0),[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(s(0))),cons(0,cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(0,cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(0),cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(0,cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(0,cons(0,[]))))) = s(s(s(s(0)))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(0,cons(s(0),[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(0),cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(0,cons(0,[]))))) = s(s(s(s(s(0))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(0,cons(s(0),[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(0),cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(s(0))))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(0,cons(0,[]))))) = s(s(s(s(s(s(0)))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(0,cons(s(0),[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(0,cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(0,cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),cons(0,[]))))) = s(s(s(s(s(s(s(0))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),cons(0,[]))))) = s(s(s(s(s(s(s(s(0)))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(s(0))))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),cons(0,[]))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(0),[]))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(0)),[]))))) = s(s(s(s(s(s(s(s(s(s(s(0))))))))))) . eq sum(cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),cons(s(s(s(0))),[]))))) = s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) . endfm