fmod INSERT is 
	sorts MyNat MyBool MyList InVec .
	 
	*** DT definitions (constructors)
	op t : -> MyBool [ctor] .
	op f : -> MyBool [ctor] .
	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 ins : MyNat MyList -> MyList [metadata "induce"] .
	op lt  : MyNat MyNat -> MyBool [metadata "pred nomatch"] .
	*** input encapsulation
	op in : MyNat MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyNat .

	eq ins(s(0),[]) = cons(s(0),[]) .
	eq ins(s(s(0)),[]) = cons(s(s(0)),[]) .
	eq ins(s(s(s(0))),[]) = cons(s(s(s(0))),[]) .
	eq ins(s(s(s(s(0)))),[]) = cons(s(s(s(s(0)))),[]) .
	eq ins(s(s(0)),cons(s(0),[])) = cons(s(0),cons(s(s(0)),[])) .
	eq ins(s(s(s(0))),cons(s(0),[])) = cons(s(0),cons(s(s(s(0))),[])) .
	eq ins(s(s(s(s(0)))),cons(s(0),[])) = cons(s(0),cons(s(s(s(s(0)))),[])) .
	eq ins(s(0),cons(s(s(0)),[])) = cons(s(0),cons(s(s(0)),[])) .
	eq ins(s(s(s(0))),cons(s(s(0)),[])) = cons(s(s(0)),cons(s(s(s(0))),[])) .
	eq ins(s(s(s(s(0)))),cons(s(s(0)),[])) = cons(s(s(0)),cons(s(s(s(s(0)))),[])) .
	eq ins(s(0),cons(s(s(s(0))),[])) = cons(s(0),cons(s(s(s(0))),[])) .
	eq ins(s(s(0)),cons(s(s(s(0))),[])) = cons(s(s(0)),cons(s(s(s(0))),[])) .
	eq ins(s(s(s(0))),cons(s(0),cons(s(s(0)),[]))) = cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[]))) .
	eq ins(s(s(s(s(0)))),cons(s(s(s(0))),[])) = cons(s(s(s(0))),cons(s(s(s(s(0)))),[])) .
	eq ins(s(0),cons(s(s(s(s(0)))),[])) = cons(s(0),cons(s(s(s(s(0)))),[])) .
	eq ins(s(s(0)),cons(s(s(s(s(0)))),[])) = cons(s(s(0)),cons(s(s(s(s(0)))),[])) .
	eq ins(s(s(s(0))),cons(s(s(s(s(0)))),[])) = cons(s(s(s(0))),cons(s(s(s(s(0)))),[])) .
	eq ins(s(s(s(s(0)))),cons(s(0),cons(s(s(s(0))),[]))) = cons(s(0),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(0),cons(s(s(0)),cons(s(s(s(0))),[]))) = cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[]))) .
	eq ins(s(s(0)),cons(s(0),cons(s(s(s(s(0)))),[]))) = cons(s(0),cons(s(s(0)),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(s(s(0))),cons(s(0),cons(s(s(s(s(0)))),[]))) = cons(s(0),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(s(s(s(0)))),cons(s(s(0)),cons(s(s(s(0))),[]))) = cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(0),cons(s(s(0)),cons(s(s(s(s(0)))),[]))) = cons(s(0),cons(s(s(0)),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(s(s(0))),cons(s(s(0)),cons(s(s(s(s(0)))),[]))) = cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(s(s(s(0)))),cons(s(0),cons(s(s(0)),cons(s(s(s(0))),[])))) = cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[])))) .
	eq ins(s(0),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) = cons(s(0),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) = cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[]))) .
	eq ins(s(s(s(0))),cons(s(0),cons(s(s(0)),cons(s(s(s(s(0)))),[])))) = cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[])))) .
	eq ins(s(s(0)),cons(s(0),cons(s(s(s(0))),cons(s(s(s(s(0)))),[])))) = cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[])))) .
	eq ins(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[])))) = cons(s(0),cons(s(s(0)),cons(s(s(s(0))),cons(s(s(s(s(0)))),[])))) .

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

endfm