fmod ADD is sorts MyNat InVec . *** DT definitions (constructors) op 0 : -> MyNat [ctor] . op s : MyNat -> MyNat [ctor] . op add : MyNat MyNat -> MyNat [metadata "induce"] . *** input encapsulation op in : MyNat MyNat -> InVec [ctor] . eq add(0,0) = 0 . eq add(s(0),0) = s(0) . eq add(s(s(0)),0) = s(s(0)) . eq add(s(s(s(0))),0) = s(s(s(0))) . eq add(s(s(s(s(0)))),0) = s(s(s(s(0)))) . eq add(s(s(s(s(s(0))))),0) = s(s(s(s(s(0))))) . eq add(0,s(0)) = s(0) . eq add(s(0),s(0)) = s(s(0)) . eq add(s(s(0)),s(0)) = s(s(s(0))) . eq add(s(s(s(0))),s(0)) = s(s(s(s(0)))) . eq add(s(s(s(s(0)))),s(0)) = s(s(s(s(s(0))))) . eq add(s(s(s(s(s(0))))),s(0)) = s(s(s(s(s(s(0)))))) . eq add(0,s(s(0))) = s(s(0)) . eq add(s(0),s(s(0))) = s(s(s(0))) . eq add(s(s(0)),s(s(0))) = s(s(s(s(0)))) . eq add(s(s(s(0))),s(s(0))) = s(s(s(s(s(0))))) . eq add(s(s(s(s(0)))),s(s(0))) = s(s(s(s(s(s(0)))))) . eq add(s(s(s(s(s(0))))),s(s(0))) = s(s(s(s(s(s(s(0))))))) . eq add(0,s(s(s(0)))) = s(s(s(0))) . eq add(s(0),s(s(s(0)))) = s(s(s(s(0)))) . eq add(s(s(0)),s(s(s(0)))) = s(s(s(s(s(0))))) . eq add(s(s(s(0))),s(s(s(0)))) = s(s(s(s(s(s(0)))))) . eq add(s(s(s(s(0)))),s(s(s(0)))) = s(s(s(s(s(s(s(0))))))) . eq add(s(s(s(s(s(0))))),s(s(s(0)))) = s(s(s(s(s(s(s(s(0)))))))) . eq add(0,s(s(s(s(0))))) = s(s(s(s(0)))) . eq add(s(0),s(s(s(s(0))))) = s(s(s(s(s(0))))) . eq add(s(s(0)),s(s(s(s(0))))) = s(s(s(s(s(s(0)))))) . eq add(s(s(s(0))),s(s(s(s(0))))) = s(s(s(s(s(s(s(0))))))) . eq add(s(s(s(s(0)))),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))) . eq add(s(s(s(s(s(0))))),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq add(0,s(s(s(s(s(0)))))) = s(s(s(s(s(0))))) . eq add(s(0),s(s(s(s(s(0)))))) = s(s(s(s(s(s(0)))))) . eq add(s(s(0)),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(0))))))) . eq add(s(s(s(0))),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(s(0)))))))) . eq add(s(s(s(s(0)))),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(s(s(0))))))))) . eq add(s(s(s(s(s(0))))),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(s(s(s(0)))))))))) . endfm