fmod SORT 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 sort : MyList -> MyList [metadata "induce"] . op lt : MyNat MyNat -> MyBool [metadata "pred nomatch"] . op ins : MyNat MyList -> MyList [metadata "pred nomatch"] . *** input encapsulation op in : MyList -> InVec [ctor] . eq sort([]) = [] . eq sort(cons(s(0),[])) = cons(s(0),[]) . eq sort(cons(s(s(0)),[])) = cons(s(s(0)),[]) . eq sort(cons(s(0),cons(s(s(0)),[]))) = cons(s(0),cons(s(s(0)),[])) . eq ins(0,[]) = cons(0,[]) . eq ins(s(0),[]) = cons(s(0),[]) . eq ins(s(s(0)),[]) = cons(s(s(0)),[]) . eq ins(0,cons(s(0),[])) = cons(0,cons(s(0),[])) . eq ins(s(s(0)),cons(s(0),[])) = cons(s(0),cons(s(s(0)),[])) . eq ins(0,cons(s(s(0)),[])) = cons(0,cons(s(s(0)),[])) . eq ins(s(0),cons(s(s(0)),[])) = cons(s(0),cons(s(s(0)),[])) . eq ins(0,cons(s(0),cons(s(s(0)),[]))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq lt(0,0) = f . eq lt(s(0),0) = f . eq lt(s(s(0)),0) = f . eq lt(0,s(0)) = t . eq lt(s(0),s(0)) = f . eq lt(s(s(0)),s(0)) = f . eq lt(0,s(s(0))) = t . eq lt(s(0),s(s(0))) = t . eq lt(s(s(0)),s(s(0))) = f . eq lt(0,s(s(s(0)))) = t . eq lt(s(0),s(s(s(0)))) = t . eq lt(s(s(0)),s(s(s(0)))) = t . endfm fmod SORT2 is sorts MyNat MyList InVec . *** DT definitions (constructors) op [] : -> MyList [ctor] . op cons : MyNat MyList -> MyList [ctor] . op 0 : -> MyNat [ctor] . op s : MyNat -> MyNat [ctor] . op Sort : MyList -> MyList [metadata "induce"] . op Ins : MyNat MyList -> MyList [metadata ""] . *** input encapsulation op in : MyList -> InVec [ctor] . op in : MyNat MyList -> InVec [ctor] . eq Sort([]) = [] . vars X Y : MyNat . var L : MyList . ***eq Sort(cons(0,[])) = cons(0,[]) . ***eq Sort(cons(s(0),[])) = cons(s(0),[]) . ***eq Sort(cons(s(s(0)),[])) = cons(s(s(0)),[]) . eq Sort(cons(X,[])) = cons(X,[]) . eq Sort(cons(0,cons(s(0),[]))) = cons(0,cons(s(0),[])) . eq Sort(cons(0,cons(s(s(0)),[]))) = cons(0,cons(s(s(0)),[])) . eq Sort(cons(s(0),cons(0,[]))) = cons(0,cons(s(0),[])) . eq Sort(cons(s(0),cons(s(s(0)),[]))) = cons(s(0),cons(s(s(0)),[])) . eq Sort(cons(s(s(0)),cons(0,[]))) = cons(0,cons(s(s(0)),[])) . eq Sort(cons(s(s(0)),cons(s(0),[]))) = cons(s(0),cons(s(s(0)),[])) . eq Sort(cons(0,cons(s(0),cons(s(s(0)),[])))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq Sort(cons(0,cons(s(s(0)),cons(s(0),[])))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq Sort(cons(s(0),cons(0,cons(s(s(0)),[])))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq Sort(cons(s(0),cons(s(s(0)),cons(0,[])))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq Sort(cons(s(s(0)),cons(0,cons(s(0),[])))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq Sort(cons(s(s(0)),cons(s(0),cons(0,[])))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . ***eq Ins(0,[]) = cons(0,[]) . ***eq Ins(s(0),[]) = cons(s(0),[]) . ***eq Ins(s(s(0)),[]) = cons(s(s(0)),[]) . eq Ins(X,[]) = cons(X,[]) . ***eq Ins(0,cons(s(0),[])) = cons(0,cons(s(0),[])) . ***eq Ins(0,cons(s(s(0)),[])) = cons(0,cons(s(s(0)),[])) . eq Ins(0,cons(Y,L)) = cons(0,cons(Y,L)) . eq Ins(s(0),cons(0,[])) = cons(0,cons(s(0),[])) . eq Ins(s(0),cons(s(s(0)),[])) = cons(s(0),cons(s(s(0)),[])) . eq Ins(s(s(0)),cons(0,[])) = cons(0,cons(s(s(0)),[])) . eq Ins(s(s(0)),cons(s(0),[])) = cons(s(0),cons(s(s(0)),[])) . ***eq Ins(0,cons(s(0),cons(s(s(0)),[]))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq Ins(s(0),cons(0,cons(s(s(0)),[]))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . eq Ins(s(s(0)),cons(0,cons(s(0),[]))) = cons(0,cons(s(0),cons(s(s(0)),[]))) . endfm