fmod ACK is 
	sorts MyNat InVec .

	*** DT definitions (constructors)
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	 
	op ack : MyNat MyNat -> MyNat [metadata "induce"] .
	 
	*** input encapsulation
	op in : MyNat MyNat -> InVec [ctor] .

	eq ack(0,0) = s(0) .
	eq ack(s(0),0) = s(s(0)) .
	eq ack(s(s(0)),0) = s(s(s(0))) .
	eq ack(s(s(s(0))),0) = s(s(s(s(s(0))))) .
	eq ack(0,s(0)) = s(s(0)) .
	eq ack(s(0),s(0)) = s(s(s(0))) .
	eq ack(s(s(0)),s(0)) = s(s(s(s(s(0))))) .
	eq ack(s(s(s(0))),s(0)) = s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))) .
	eq ack(0,s(s(0))) = s(s(s(0))) .
	eq ack(s(0),s(s(0))) = s(s(s(s(0)))) .
	eq ack(s(s(0)),s(s(0))) = s(s(s(s(s(s(s(0))))))) .
	eq ack(s(s(s(0))),s(s(0))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))))))))))))))) .
	eq ack(0,s(s(s(0)))) = s(s(s(s(0)))) .
	eq ack(s(0),s(s(s(0)))) = s(s(s(s(s(0))))) .
	eq ack(s(s(0)),s(s(s(0)))) = s(s(s(s(s(s(s(s(s(0))))))))) .
	eq ack(s(s(s(0))),s(s(s(0)))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) .
	eq ack(0,s(s(s(s(0))))) = s(s(s(s(s(0))))) .
	eq ack(s(0),s(s(s(s(0))))) = s(s(s(s(s(s(0)))))) .
	eq ack(s(s(0)),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(s(s(s(0))))))))))) .
	eq ack(s(s(s(0))),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) .
endfm