fmod GEQ is 
	sorts MyNat MyBool InVec .
	 
	*** DT definitions (constructors)
	op t : -> MyBool [ctor] .
	op f : -> MyBool [ctor] .
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	 
	op geq : MyNat MyNat -> MyBool [metadata "induce"] .
	 
	*** input encapsulation
	op in : MyNat MyNat -> InVec [ctor] .

	eq geq(0,0) = t .
	eq geq(s(0),0) = t .
	eq geq(s(s(0)),0) = t .
	eq geq(s(s(s(0))),0) = t .
	eq geq(s(s(s(s(0)))),0) = t .
	eq geq(s(s(s(s(s(0))))),0) = t .
	eq geq(0,s(0)) = f .
	eq geq(s(0),s(0)) = t .
	eq geq(s(s(0)),s(0)) = t .
	eq geq(s(s(s(0))),s(0)) = t .
	eq geq(s(s(s(s(0)))),s(0)) = t .
	eq geq(s(s(s(s(s(0))))),s(0)) = t .
	eq geq(0,s(s(0))) = f .
	eq geq(s(0),s(s(0))) = f .
	eq geq(s(s(0)),s(s(0))) = t .
	eq geq(s(s(s(0))),s(s(0))) = t .
	eq geq(s(s(s(s(0)))),s(s(0))) = t .
	eq geq(s(s(s(s(s(0))))),s(s(0))) = t .
	eq geq(0,s(s(s(0)))) = f .
	eq geq(s(0),s(s(s(0)))) = f .
	eq geq(s(s(0)),s(s(s(0)))) = f .
	eq geq(s(s(s(0))),s(s(s(0)))) = t .
	eq geq(s(s(s(s(0)))),s(s(s(0)))) = t .
	eq geq(s(s(s(s(s(0))))),s(s(s(0)))) = t .
	eq geq(0,s(s(s(s(0))))) = f .
	eq geq(s(0),s(s(s(s(0))))) = f .
	eq geq(s(s(0)),s(s(s(s(0))))) = f .
	eq geq(s(s(s(0))),s(s(s(s(0))))) = f .
	eq geq(s(s(s(s(0)))),s(s(s(s(0))))) = t .
	eq geq(s(s(s(s(s(0))))),s(s(s(s(0))))) = t .
	eq geq(0,s(s(s(s(s(0)))))) = f .
	eq geq(s(0),s(s(s(s(s(0)))))) = f .
	eq geq(s(s(0)),s(s(s(s(s(0)))))) = f .
	eq geq(s(s(s(0))),s(s(s(s(s(0)))))) = f .
	eq geq(s(s(s(s(0)))),s(s(s(s(s(0)))))) = f .
	eq geq(s(s(s(s(s(0))))),s(s(s(s(s(0)))))) = t .

endfm