*** LIST OPERATIONS *******************************************************************************


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

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


fmod APPEND is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op app : MyList MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList MyList -> InVec [ctor] .
	 
	vars W X Y Z : MyItem .

	eq app([],[]) = [] .
	eq app(cons(W,[]),[]) = cons(W,[]) .
	eq app(cons(W,cons(X,[])),[]) = cons(W,cons(X,[])) .
	eq app([],cons(Y,[])) = cons(Y,[]) .
	eq app(cons(W,[]),cons(Z,[])) = cons(W,cons(Z,[])) .
	eq app(cons(W,cons(X,[])),cons(Z,[])) = cons(W,cons(X,cons(Z,[]))) .
	eq app([],cons(Y,cons(Z,[]))) = cons(Y,cons(Z,[])) .
	eq app(cons(W,[]),cons(Z,cons(Y,[]))) = cons(W,cons(Z,cons(Y,[]))) .
	eq app(cons(W,cons(X,[])),cons(Z,cons(Y,[]))) = cons(W,cons(X,cons(Z,cons(Y,[])))) .
endfm


fmod CAR is 
	sorts MyItem MyList MyNat InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op car : MyList -> MyItem [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z F : MyItem .

	eq car(cons(Y,[])) = Y .
	eq car(cons(X,cons(Y,[]))) = X .
	eq car(cons(Y,cons(X,cons(Z,[])))) = Y .
	eq car(cons(Y,cons(X,cons(Z,[])))) = Y .
	eq car(cons(F, cons(Y,cons(X,cons(Z,[]))))) = F .
endfm


fmod CDR is 
	sorts MyItem MyList MyNat InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op cdr : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z F : MyItem .

	*** eq cdr([]) =  [].
	eq cdr(cons(Y,[])) = [] .
	eq cdr(cons(X,cons(Y,[]))) = cons(Y, []) .
	eq cdr(cons(Y,cons(X,cons(Z,[])))) = cons(X, cons(Z, [])).
	eq cdr(cons(F, cons(Y,cons(X,cons(Z,[]))))) = cons(Y, cons(X, cons(Z, []))).
endfm


fmod CLEARBLOCK is
	sorts Block Tower State InVec .
	
	op table : -> Tower [ctor] .
	op __ : Block Tower -> Tower [ctor] .
	
	op putt : Block State -> State [ctor] .		*** put to table
	
	op ClearBlock : Block Tower State -> State [metadata "induce"] .
	op in : Block Tower State -> InVec [ctor] .
	
	*** solution
	*** ClearBlock(A, B T, S) = S if A == B
	*** ClearBlock(A, B T, S) = ClearBlock(A, T, putt(B, S))
	
	vars A B C : Block .
	var S : State .
	
	*** examples
	*** second example indicates that the block to be cleared need not
	*** be the bottom block
	eq ClearBlock(A, A table, S) = S .
	eq ClearBlock(A, A B table, S) = S .
	eq ClearBlock(A, B A table, S) = putt(B, S) .
	eq ClearBlock(A, C B A table, S) = putt(B, putt(C, S)) .
endfm


fmod DROP is 
	sorts MyItem MyNat MyList InVec .
	 
	*** DT definitions (constructors)
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op drop : MyNat MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyNat MyList -> InVec [ctor] .
	 
	vars W X Y Z : MyItem .

	eq drop(0,[]) = [] .
	eq drop(s(0),[]) = [] .
	eq drop(s(s(0)),[]) = [] .
	eq drop(s(s(s(0))),[]) = [] .
	%eq drop(s(s(s(s(0)))),[]) = [] .
	eq drop(0,cons(X,[])) = cons(X,[]) .
	eq drop(s(0),cons(X,[])) = [] .
	eq drop(s(s(0)),cons(X,[])) = [] .
	eq drop(s(s(s(0))),cons(X,[])) = [] .
	%eq drop(s(s(s(s(0)))),cons(X,[])) = [] .
	eq drop(0,cons(X,cons(Y,[]))) = cons(X,cons(Y,[])) .
	eq drop(s(0),cons(X,cons(Y,[]))) = cons(Y,[]) .
	eq drop(s(s(0)),cons(X,cons(Y,[]))) = [] .
	eq drop(s(s(s(0))),cons(X,cons(Y,[]))) = [] .
	%eq drop(s(s(s(s(0)))),cons(X,cons(Y,[]))) = [] .
	eq drop(0,cons(X,cons(Y,cons(Z,[])))) = cons(X,cons(Y,cons(Z,[]))) .
	eq drop(s(0),cons(X,cons(Y,cons(Z,[])))) = cons(Y,cons(Z,[])) .
	eq drop(s(s(0)),cons(X,cons(Y,cons(Z,[])))) = cons(Z,[]) .
	eq drop(s(s(s(0))),cons(X,cons(Y,cons(Z,[])))) = [] .
	%eq drop(s(s(s(s(0)))),cons(X,cons(Y,cons(Z,[])))) = [] .
	eq drop(0,cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,cons(X,cons(Z,cons(Y,[])))) .
	eq drop(s(0),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(X,cons(Z,cons(Y,[]))) .
	eq drop(s(s(0)),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Z,cons(Y,[])) .
	eq drop(s(s(s(0))),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,[]) .
	%eq drop(s(s(s(s(0)))),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = [] .
endfm


fmod EQ 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 eq : MyNat MyNat -> MyBool [metadata "induce"] .
	 
	*** input encapsulation
	op in : MyNat MyNat -> InVec [ctor] .

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

endfm


fmod EVEN is
	sorts MyNat MyBool InVec .
	
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	op t : -> MyBool [ctor] .
	op f : -> MyBool [ctor] .
	
	op Even : MyNat -> MyBool [metadata "induce"] .
	op in : MyNat -> InVec [ctor] .
	
	eq Even(0) = t .
	eq Even(s(0)) = f .
	eq Even(s(s(0))) = t .
endfm


fmod EVENLIST is 
	sorts MyItem MyBool MyList InVec .
	 
	*** DT definitions (constructors)
	op t : -> MyBool [ctor] .
	op f : -> MyBool [ctor] .
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op evenlist : MyList -> MyBool [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars X Y Z : MyItem .

	eq evenlist([]) = t .
	eq evenlist(cons(X,[])) = f .
	eq evenlist(cons(X,cons(Y,[]))) = t .
	eq evenlist(cons(X,cons(Y,cons(Z,[])))) = f .
	eq evenlist(cons(Y,cons(X,cons(Z,cons(Y,[]))))) = t .
	eq evenlist(cons(X,cons(X,cons(Y,cons(Z,cons(X,[])))))) = f .

endfm


fmod EVENODD is
	sorts MyNat MyBool InVec .
	
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	op t : -> MyBool [ctor] .
	op f : -> MyBool [ctor] .
	
	op Even : MyNat -> MyBool [metadata "induce"] .
	op Odd : MyNat -> MyBool [metadata "induce"] .
	op in : MyNat -> InVec [ctor] .
	
	eq Even(0) = t .
	eq Even(s(0)) = f .
	eq Even(s(s(0))) = t .
	
	eq Odd(0) = f .
	eq Odd(s(0)) = t .
	eq Odd(s(s(0))) = f .
	***eq Odd(s(s(s(0)))) = t .
endfm


fmod EVENPOS is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op evenpos : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq evenpos([]) = [] .
	eq evenpos(cons(X,[])) = [] .
	eq evenpos(cons(X,cons(Z,[]))) = cons(Z,[]) .
	eq evenpos(cons(X,cons(V,cons(Z,[])))) = cons(V,[]) .
	eq evenpos(cons(X,cons(Z,cons(Y,cons(U,[]))))) = cons(Z,cons(U,[])) .
	eq evenpos(cons(X,cons(W,cons(Z,cons(U,cons(Y,[])))))) = cons(W,cons(U,[])) .
	eq evenpos(cons(X,cons(W,cons(Z,cons(U,cons(Y,cons(V,[]))))))) = cons(W,cons(U,cons(V,[]))) .

endfm


fmod EVENSLIST 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 evenslist : MyList -> MyBool [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars X Y Z : MyNat .

	eq evenslist([]) = f .
	eq evenslist(cons(s(0),[])) = f .
	eq evenslist(cons(0,[])) = t .
	eq evenslist(cons(s(s(0)),[])) = t .
	eq evenslist(cons(s(s(s(0))),[])) = f .
	eq evenslist(cons(0,cons(0,[]))) = t .
	eq evenslist(cons(0,cons(s(0),[]))) = t .
	eq evenslist(cons(0,cons(s(s(0)),[]))) = t .
	eq evenslist(cons(0,cons(s(s(s(0))),[]))) = t .
	eq evenslist(cons(s(0),cons(0,[]))) = f .
	eq evenslist(cons(s(0),cons(s(0),[]))) = f .
	eq evenslist(cons(s(0),cons(s(s(0)),[]))) = f .
	eq evenslist(cons(s(0),cons(s(s(s(0))),[]))) = f .
	eq evenslist(cons(s(s(0)),cons(0,[]))) = t .
	eq evenslist(cons(s(s(0)),cons(s(0),[]))) = t .
	eq evenslist(cons(s(s(0)),cons(s(s(0)),[]))) = t .
	eq evenslist(cons(s(s(0)),cons(s(s(s(0))),[]))) = t .
	eq evenslist(cons(s(s(s(0))),cons(0,[]))) = t .
	eq evenslist(cons(s(s(s(0))),cons(s(0),[]))) = t .
	eq evenslist(cons(s(s(s(0))),cons(s(s(0)),[]))) = t .
	eq evenslist(cons(s(s(s(0))),cons(s(s(s(0))),[]))) = t .
endfm

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



fmod FIB is 
	sorts MyItem MyList MyNat InVec .
	 
	*** DT definitions (constructors)
	op 0 : -> MyNat [ctor] .
	op [] : -> MyList [ctor] .
	op succ : MyNat -> MyNat [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op fib : MyNat -> MyNat [metadata "induce"] .
	*** input encapsulation
	op in : MyNat -> InVec [ctor] .

	eq fib(0) = 0 .
	eq fib(succ(0)) = succ(0) .
	eq fib(succ(succ(0)) ) = succ(0) .
	eq fib(succ(succ(succ(0)))) = succ(succ(0)) .
	eq fib(succ(succ(succ(succ(0))))) = succ(succ(succ(0))).
endfm

fmod HANOI is
	sorts Disc Peg State InVec .
	
	op 0 : -> Disc [ctor] .			*** smallest disc
	op s_ : Disc -> Disc [ctor] .	*** next bigger disc
	
	*** move disc from one peg to another in a current state
	op move : Disc Peg Peg State -> State [ctor] .
	
	*** move tower up to specified disc from start peg via aux peg to
	*** goal peg in a given state
	op Hanoi : Disc Peg Peg Peg State -> State [metadata "induce"] .
	op in : Disc Peg Peg Peg State -> InVec [ctor] .
	
	*** solution
	*** Hanoi(0, Src, Aux, Dst, S) = move(0, Src, Dst, S)
	*** Hanoi(s D, Src, Aux, Dst, S) = 
	***		Hanoi(D, Aux, Src, Dst, 
	***			move(s D, Src, Dst, 
	***				Hanoi(D, Src, Dst, Aux, S)))
	
	var S : State .
	vars Src Aux Dst : Peg .
	
	eq Hanoi(0, Src, Aux, Dst, S) = move(0, Src, Dst, S) .
	eq Hanoi(s 0, Src, Aux, Dst, S) = 
		move(0, Aux, Dst, move(s 0, Src, Dst, move(0, Src, Aux, S))) .
	eq Hanoi(s s 0, Src, Aux, Dst, S) = 
		move(0, Src, Dst, 
			move(s 0, Aux, Dst,
				move(0, Aux, Src,
					move(s s 0, Src, Dst, 
						move(0, Dst, Aux,
							move(s 0, Src, Aux,
								move(0, Src, Dst, S))))))) .
endfm


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


fmod LAST is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op last : MyList -> MyItem [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq last(cons(Y,[])) = Y .
	eq last(cons(Y,cons(X,[]))) = X .
	eq last(cons(Y,cons(X,cons(Z,[])))) = Z .
endfm


fmod LASTS is 
	sorts MyItem MyList MyLList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	op # : -> MyLList [ctor] .
	op consl : MyList MyLList -> MyLList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op lasts : MyLList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyLList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq lasts(#) = [] .
	eq lasts(consl(cons(Y,[]),#)) = cons(Y,[]) .
	eq lasts(consl(cons(Y,cons(X,[])),#)) = cons(X,[]) .
	eq lasts(consl(cons(Y,cons(X,cons(Z,[]))),#)) = cons(Z,[]) .
	eq lasts(consl(cons(Y,[]),consl(cons(X,[]),#))) = cons(Y,cons(X,[])) .
	eq lasts(consl(cons(X,[]),consl(cons(Y,cons(Z,[])),#))) = cons(X,cons(Z,[])) .
	eq lasts(consl(cons(X,cons(V,[])),consl(cons(Y,cons(Z,[])),#))) = cons(V,cons(Z,[])) .
	eq lasts(consl(cons(X,cons(V,[])),consl(cons(Z,[]),#))) = cons(V,cons(Z,[])) .
	eq lasts(consl(cons(Z,[]),consl(cons(Y,cons(X,[])),consl(cons(V,[]),#)))) = cons(Z,cons(X,cons(V,[]))) .
	eq lasts(consl(cons(Z,cons(X,[])),consl(cons(Y,cons(V,[])),consl(cons(W,[]),#)))) = cons(X,cons(V,cons(W,[]))) .
	***eq lasts(consl(cons(Z,cons(X,[])),consl(cons(V,cons(Y,[])),consl(cons(W,cons(U,[])),#)))) = cons(X,cons(Y,cons(U,[]))) .
endfm


fmod LENGTH is 
	sorts MyItem MyList MyNat InVec .
	 
	*** DT definitions (constructors)
	op 0 : -> MyNat [ctor] .
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	op succ : MyNat -> MyNat [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op length : MyList -> MyNat [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq length([]) = 0 .
	eq length(cons(Y,[])) = succ(0) .
	eq length(cons(Y,cons(X,[]))) = succ(succ(0)) .
	eq length(cons(Y,cons(X,cons(Z,[])))) = succ(succ(succ(0))) .
endfm




fmod MEMBER is 
	sorts MyItem MyBool MyList InVec .
	 
	*** DT definitions (constructors)
	op t : -> MyBool [ctor] .
	op f : -> MyBool [ctor] .
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op mem : MyItem MyList -> MyBool [metadata "induce"] .
	*** input encapsulation
	op in : MyItem MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq mem(W,[]) = f .
	eq mem(W,cons(Y,[])) = f .
	eq mem(W,cons(Y,cons(Z,[]))) = f .
	eq mem(Y,cons(X,cons(Y,cons(W,[])))) = t .
endfm


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

	eq mult(0,0) = 0 .
	eq mult(s(0),0) = 0 .
	eq mult(s(s(0)),0) = 0 .
	eq mult(s(s(s(0))),0) = 0 .
	eq mult(s(s(s(s(0)))),0) = 0 .
	eq mult(0,s(0)) = 0 .
	eq mult(s(0),s(0)) = s(0) .
	eq mult(s(s(0)),s(0)) = s(s(0)) .
	eq mult(s(s(s(0))),s(0)) = s(s(s(0))) .
	eq mult(s(s(s(s(0)))),s(0)) = s(s(s(s(0)))) .
	eq mult(0,s(s(0))) = 0 .
	eq mult(s(0),s(s(0))) = s(s(0)) .
	eq mult(s(s(0)),s(s(0))) = s(s(s(s(0)))) .
	eq mult(s(s(s(0))),s(s(0))) = s(s(s(s(s(s(0)))))) .
	eq mult(s(s(s(s(0)))),s(s(0))) = s(s(s(s(s(s(s(s(0)))))))) .
	eq mult(0,s(s(s(0)))) = 0 .
	eq mult(s(0),s(s(s(0)))) = s(s(s(0))) .
	eq mult(s(s(0)),s(s(s(0)))) = s(s(s(s(s(s(0)))))) .
	eq mult(s(s(s(0))),s(s(s(0)))) = s(s(s(s(s(s(s(s(s(0))))))))) .
	eq mult(s(s(s(s(0)))),s(s(s(0)))) = s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) .
	eq mult(0,s(s(s(s(0))))) = 0 .
	eq mult(s(0),s(s(s(s(0))))) = s(s(s(s(0)))) .
	eq mult(s(s(0)),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))) .
	eq mult(s(s(s(0))),s(s(s(s(0))))) = s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))) .
	eq mult(s(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(0)))))))))))))))) .

endfm


fmod MULTADD is
	sorts MyNat InVec .

	*** DT definitions (constructors)
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .

	op Mult : MyNat MyNat -> MyNat [metadata "induce"] .
	op Add : MyNat MyNat -> MyNat [metadata "induce"] .
	
	*** input encapsulation
	op in : MyNat MyNat -> InVec [ctor] .

	vars X Y : MyNat .
	
	***eq Add(0,X) = X .
	***eq Add(s(0),X) = s(X) .
	***eq Add(s(s(0)),X) = s(s(X)) .
	
	***eq Add(0,0) = 0 .
	***eq Add(s(0),0) = s(0) .
	***eq Add(s(s(0)),0) = 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(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 Mult(0,s(0)) = 0 .
	eq Mult(0,0) = 0 .
	eq Mult(s(0),s(0)) = s(0) .
	eq Mult(s(s(0)),s(0)) = s(s(0)) .
	***eq Mult(X,0) = 0 .
	***eq Mult(0,s(s(0))) = 0 .
	***eq Mult(0,s(X)) = 0 .
	eq Mult(s(0),s(s(0))) = s(s(0)) .
	eq Mult(s(s(0)),s(s(0))) = s(s(s(s(0)))) .
	***eq Mult(s(s(0)),s(0)) = s(s(0)) .
	***eq Mult(0,s(s(0))) = 0 .
	***eq Mult(s(0),s(s(0))) = s(s(0)) .
endfm



fmod MULTFIRST is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op multfirst : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq multfirst([]) = [] .
	eq multfirst(cons(Y,[])) = cons(Y,[]) .
	eq multfirst(cons(Y,cons(X,[]))) = cons(Y,cons(Y,[])) .
	eq multfirst(cons(Y,cons(X,cons(Z,[])))) = cons(Y,cons(Y,cons(Y,[]))) .
endfm


fmod MULTLAST is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op multlast : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq multlast([]) = [] .
	eq multlast(cons(Y,[])) = cons(Y,[]) .
	eq multlast(cons(Y,cons(X,[]))) = cons(X,cons(X,[])) .
	eq multlast(cons(Y,cons(X,cons(Z,[])))) = cons(Z,cons(Z,cons(Z,[]))) .
endfm


fmod ODD is
	sorts MyNat MyBool InVec .
	
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	op t : -> MyBool [ctor] .
	op f : -> MyBool [ctor] .
	
	op Odd : MyNat -> MyBool [metadata "induce"] .
	op in : MyNat -> InVec [ctor] .
	
	eq Odd(0) = f .
	eq Odd(s(0)) = t .
	eq Odd(s(s(0))) = f .
	***eq Odd(s(s(s(0)))) = t .
endfm


fmod ODDPOS is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op oddpos : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq oddpos([]) = [] .
	eq oddpos(cons(X,[])) = cons(X,[]) .
	eq oddpos(cons(X,cons(Z,[]))) = cons(X,[]) .
	eq oddpos(cons(X,cons(V,cons(Z,[])))) = cons(X, cons(Z,[]) ) .
	eq oddpos(cons(X,cons(Z,cons(Y,cons(U,[]))))) = cons(X, cons(Y,[])) .
	eq oddpos(cons(X,cons(W,cons(Z,cons(U,cons(Y,[])))))) = cons(X, cons(Z, cons(Y, []))) .
	eq oddpos(cons(X,cons(W,cons(Z,cons(U,cons(Y,cons(V,[]))))))) = cons(X, cons(Z, cons(Y, []))) .

endfm



fmod ODDSLIST 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 oddslist : MyList -> MyBool [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars X Y Z : MyNat .

	eq oddslist([]) = t .
	eq oddslist(cons(s(0),[])) = t .
	eq oddslist(cons(0,[])) = f .
	eq oddslist(cons(s(s(0)),[])) = f .
	eq oddslist(cons(s(s(s(0))),[])) = t .
	eq oddslist(cons(0,cons(0,[]))) = f .
	eq oddslist(cons(0,cons(s(0),[]))) = f .
	eq oddslist(cons(0,cons(s(s(0)),[]))) = f .
	eq oddslist(cons(0,cons(s(s(s(0))),[]))) = f .
	eq oddslist(cons(s(0),cons(0,[]))) = f .
	eq oddslist(cons(s(0),cons(s(0),[]))) = t .
	eq oddslist(cons(s(0),cons(s(s(0)),[]))) = t .
	eq oddslist(cons(s(0),cons(s(s(s(0))),[]))) = t .
	eq oddslist(cons(s(s(0)),cons(0,[]))) = f .
	eq oddslist(cons(s(s(0)),cons(s(0),[]))) = f .
	eq oddslist(cons(s(s(0)),cons(s(s(0)),[]))) = f .
	eq oddslist(cons(s(s(0)),cons(s(s(s(0))),[]))) = f .
	eq oddslist(cons(s(s(s(0))),cons(0,[]))) = f .
	eq oddslist(cons(s(s(s(0))),cons(s(0),[]))) = f .
	eq oddslist(cons(s(s(s(0))),cons(s(s(0)),[]))) = f .
	eq oddslist(cons(s(s(s(0))),cons(s(s(s(0))),[]))) = f .
endfm


fmod REVERSE is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op reverse : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq reverse([]) = [] .
	eq reverse(cons(Y,[])) = cons(Y,[]) .
	eq reverse(cons(Y,cons(X,[]))) = cons(X,cons(Y,[])) .
	eq reverse(cons(Y,cons(X,cons(Z,[])))) = cons(Z,cons(X,cons(Y,[]))) .
endfm



fmod SHIFTL is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op shiftl : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq shiftl([]) = [] .
	eq shiftl(cons(W,[])) = cons(W,[]) .
	eq shiftl(cons(Y,cons(Z,[]))) = cons(Z,cons(Y,[])) .
	eq shiftl(cons(X,cons(Z,cons(W,[])))) = cons(Z,cons(W,cons(X,[]))) .
	eq shiftl(cons(X,cons(Z,cons(W,cons(Y,[]))))) = cons(Z,cons(W,cons(Y,cons(X,[])))) .
endfm


fmod SHIFTR is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op shiftr : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq shiftr([]) = [] .
	eq shiftr(cons(W,[])) = cons(W,[]) .
	eq shiftr(cons(Y,cons(Z,[]))) = cons(Z,cons(Y,[])) .
	eq shiftr(cons(X,cons(Z,cons(W,[])))) = cons(W,cons(X,cons(Z,[]))) .
	eq shiftr(cons(X,cons(Z,cons(W,cons(Y,[]))))) = cons(Y,cons(X,cons(Z,cons(W,[])))) .
endfm


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

fmod SUM is 
	sorts MyNat MyList InVec .
	 
	*** DT definitions (constructors)
	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 sum : MyList -> MyNat [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .

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

endfm


fmod SWAP is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op swap : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq swap([]) = [] .
	eq swap(cons(V,[])) = cons(V,[]) .
	eq swap(cons(X,cons(W,[]))) = cons(W,cons(X,[])) .
	eq swap(cons(V,cons(Z,cons(W,[])))) = cons(W,cons(Z,cons(V,[]))) .
	eq swap(cons(V,cons(Z,cons(W,cons(Y,[]))))) = cons(Y,cons(Z,cons(W,cons(V,[])))) .
	eq swap(cons(V,cons(Z,cons(W,cons(Y,cons(X,[])))))) = cons(X,cons(Z,cons(W,cons(Y,cons(V,[]))))) .

endfm


fmod SWITCH is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op switch : MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList -> InVec [ctor] .
	 
	vars U V W X Y Z : MyItem .

	eq switch([]) = [] .
	eq switch(cons(V,[])) = cons(V,[]) .
	eq switch(cons(X,cons(W,[]))) = cons(W,cons(X,[])) .
	eq switch(cons(V,cons(Z,cons(W,[])))) = cons(Z,cons(V,cons(W,[]))) .
	eq switch(cons(V,cons(Z,cons(W,cons(Y,[]))))) = cons(Z,cons(V,cons(Y,cons(W,[])))) .
	eq switch(cons(V,cons(Z,cons(W,cons(Y,cons(X,[])))))) = cons(Z,cons(V,cons(Y,cons(W,cons(X,[]))))) .

endfm


fmod TAKE is 
	sorts MyItem MyNat MyList InVec .
	 
	*** DT definitions (constructors)
	op 0 : -> MyNat [ctor] .
	op s : MyNat -> MyNat [ctor] .
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op take : MyNat MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyNat MyList -> InVec [ctor] .
	 
	vars W X Y Z : MyItem .

	eq take(0,[]) = [] .
	eq take(0,cons(X,[])) = [] .
	eq take(0,cons(Y,[])) = [] .
	eq take(0,cons(Z,[])) = [] .
	eq take(0,cons(X,cons(Y,[]))) = [] .
	eq take(0,cons(X,cons(Z,[]))) = [] .
	eq take(0,cons(Y,cons(X,[]))) = [] .
	eq take(0,cons(Y,cons(Z,[]))) = [] .
	eq take(0,cons(Z,cons(X,[]))) = [] .
	eq take(0,cons(Z,cons(Y,[]))) = [] .
	eq take(0,cons(X,cons(Y,cons(Z,[])))) = [] .
	eq take(0,cons(X,cons(Z,cons(Y,[])))) = [] .
	eq take(0,cons(Y,cons(X,cons(Z,[])))) = [] .
	eq take(0,cons(Y,cons(Z,cons(X,[])))) = [] .
	eq take(0,cons(Z,cons(X,cons(Y,[])))) = [] .
	eq take(0,cons(Z,cons(Y,cons(X,[])))) = [] .
	eq take(0,cons(X,cons(X,cons(Y,cons(Z,[]))))) = [] .
	eq take(0,cons(X,cons(X,cons(Z,cons(Y,[]))))) = [] .
	eq take(0,cons(X,cons(Y,cons(X,cons(Z,[]))))) = [] .
	eq take(0,cons(X,cons(Y,cons(Z,cons(X,[]))))) = [] .
	eq take(0,cons(X,cons(Z,cons(X,cons(Y,[]))))) = [] .
	eq take(0,cons(X,cons(Z,cons(Y,cons(X,[]))))) = [] .
	eq take(0,cons(Y,cons(X,cons(Y,cons(Z,[]))))) = [] .
	eq take(0,cons(Y,cons(X,cons(Z,cons(Y,[]))))) = [] .
	eq take(0,cons(Y,cons(Y,cons(X,cons(Z,[]))))) = [] .
	eq take(0,cons(Y,cons(Y,cons(Z,cons(X,[]))))) = [] .
	eq take(0,cons(Y,cons(Z,cons(X,cons(Y,[]))))) = [] .
	eq take(0,cons(Y,cons(Z,cons(Y,cons(X,[]))))) = [] .
	eq take(0,cons(Z,cons(X,cons(Y,cons(Z,[]))))) = [] .
	eq take(0,cons(Z,cons(X,cons(Z,cons(Y,[]))))) = [] .
	eq take(0,cons(Z,cons(Y,cons(X,cons(Z,[]))))) = [] .
	eq take(0,cons(Z,cons(Y,cons(Z,cons(X,[]))))) = [] .
	eq take(0,cons(Z,cons(Z,cons(X,cons(Y,[]))))) = [] .
	eq take(0,cons(Z,cons(Z,cons(Y,cons(X,[]))))) = [] .
	eq take(s(0),[]) = [] .
	eq take(s(0),cons(X,[])) = cons(X,[]) .
	eq take(s(0),cons(Y,[])) = cons(Y,[]) .
	eq take(s(0),cons(Z,[])) = cons(Z,[]) .
	eq take(s(0),cons(X,cons(Y,[]))) = cons(X,[]) .
	eq take(s(0),cons(X,cons(Z,[]))) = cons(X,[]) .
	eq take(s(0),cons(Y,cons(X,[]))) = cons(Y,[]) .
	eq take(s(0),cons(Y,cons(Z,[]))) = cons(Y,[]) .
	eq take(s(0),cons(Z,cons(X,[]))) = cons(Z,[]) .
	eq take(s(0),cons(Z,cons(Y,[]))) = cons(Z,[]) .
	eq take(s(0),cons(X,cons(Y,cons(Z,[])))) = cons(X,[]) .
	eq take(s(0),cons(X,cons(Z,cons(Y,[])))) = cons(X,[]) .
	eq take(s(0),cons(Y,cons(X,cons(Z,[])))) = cons(Y,[]) .
	eq take(s(0),cons(Y,cons(Z,cons(X,[])))) = cons(Y,[]) .
	eq take(s(0),cons(Z,cons(X,cons(Y,[])))) = cons(Z,[]) .
	eq take(s(0),cons(Z,cons(Y,cons(X,[])))) = cons(Z,[]) .
	eq take(s(0),cons(X,cons(X,cons(Y,cons(Z,[]))))) = cons(X,[]) .
	eq take(s(0),cons(X,cons(X,cons(Z,cons(Y,[]))))) = cons(X,[]) .
	eq take(s(0),cons(X,cons(Y,cons(X,cons(Z,[]))))) = cons(X,[]) .
	eq take(s(0),cons(X,cons(Y,cons(Z,cons(X,[]))))) = cons(X,[]) .
	eq take(s(0),cons(X,cons(Z,cons(X,cons(Y,[]))))) = cons(X,[]) .
	eq take(s(0),cons(X,cons(Z,cons(Y,cons(X,[]))))) = cons(X,[]) .
	eq take(s(0),cons(Y,cons(X,cons(Y,cons(Z,[]))))) = cons(Y,[]) .
	eq take(s(0),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,[]) .
	eq take(s(0),cons(Y,cons(Y,cons(X,cons(Z,[]))))) = cons(Y,[]) .
	eq take(s(0),cons(Y,cons(Y,cons(Z,cons(X,[]))))) = cons(Y,[]) .
	eq take(s(0),cons(Y,cons(Z,cons(X,cons(Y,[]))))) = cons(Y,[]) .
	eq take(s(0),cons(Y,cons(Z,cons(Y,cons(X,[]))))) = cons(Y,[]) .
	eq take(s(0),cons(Z,cons(X,cons(Y,cons(Z,[]))))) = cons(Z,[]) .
	eq take(s(0),cons(Z,cons(X,cons(Z,cons(Y,[]))))) = cons(Z,[]) .
	eq take(s(0),cons(Z,cons(Y,cons(X,cons(Z,[]))))) = cons(Z,[]) .
	eq take(s(0),cons(Z,cons(Y,cons(Z,cons(X,[]))))) = cons(Z,[]) .
	eq take(s(0),cons(Z,cons(Z,cons(X,cons(Y,[]))))) = cons(Z,[]) .
	eq take(s(0),cons(Z,cons(Z,cons(Y,cons(X,[]))))) = cons(Z,[]) .
	eq take(s(s(0)),[]) = [] .
	eq take(s(s(0)),cons(X,[])) = cons(X,[]) .
	eq take(s(s(0)),cons(Y,[])) = cons(Y,[]) .
	eq take(s(s(0)),cons(Z,[])) = cons(Z,[]) .
	eq take(s(s(0)),cons(X,cons(Y,[]))) = cons(X,cons(Y,[])) .
	eq take(s(s(0)),cons(X,cons(Z,[]))) = cons(X,cons(Z,[])) .
	eq take(s(s(0)),cons(Y,cons(X,[]))) = cons(Y,cons(X,[])) .
	eq take(s(s(0)),cons(Y,cons(Z,[]))) = cons(Y,cons(Z,[])) .
	eq take(s(s(0)),cons(Z,cons(X,[]))) = cons(Z,cons(X,[])) .
	eq take(s(s(0)),cons(Z,cons(Y,[]))) = cons(Z,cons(Y,[])) .
	eq take(s(s(0)),cons(X,cons(Y,cons(Z,[])))) = cons(X,cons(Y,[])) .
	eq take(s(s(0)),cons(X,cons(Z,cons(Y,[])))) = cons(X,cons(Z,[])) .
	eq take(s(s(0)),cons(Y,cons(X,cons(Z,[])))) = cons(Y,cons(X,[])) .
	eq take(s(s(0)),cons(Y,cons(Z,cons(X,[])))) = cons(Y,cons(Z,[])) .
	eq take(s(s(0)),cons(Z,cons(X,cons(Y,[])))) = cons(Z,cons(X,[])) .
	eq take(s(s(0)),cons(Z,cons(Y,cons(X,[])))) = cons(Z,cons(Y,[])) .
	eq take(s(s(0)),cons(X,cons(Y,cons(X,cons(Z,[]))))) = cons(X,cons(Y,[])) .
	eq take(s(s(0)),cons(X,cons(Y,cons(Z,cons(X,[]))))) = cons(X,cons(Y,[])) .
	eq take(s(s(0)),cons(X,cons(Z,cons(X,cons(Y,[]))))) = cons(X,cons(Z,[])) .
	eq take(s(s(0)),cons(X,cons(Z,cons(Y,cons(X,[]))))) = cons(X,cons(Z,[])) .
	eq take(s(s(0)),cons(Y,cons(X,cons(Y,cons(Z,[]))))) = cons(Y,cons(X,[])) .
	eq take(s(s(0)),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,cons(X,[])) .
	eq take(s(s(0)),cons(Y,cons(Z,cons(X,cons(Y,[]))))) = cons(Y,cons(Z,[])) .
	eq take(s(s(0)),cons(Y,cons(Z,cons(Y,cons(X,[]))))) = cons(Y,cons(Z,[])) .
	eq take(s(s(0)),cons(Z,cons(X,cons(Y,cons(Z,[]))))) = cons(Z,cons(X,[])) .
	eq take(s(s(0)),cons(Z,cons(X,cons(Z,cons(Y,[]))))) = cons(Z,cons(X,[])) .
	eq take(s(s(0)),cons(Z,cons(Y,cons(X,cons(Z,[]))))) = cons(Z,cons(Y,[])) .
	eq take(s(s(0)),cons(Z,cons(Y,cons(Z,cons(X,[]))))) = cons(Z,cons(Y,[])) .
	eq take(s(s(s(0))),[]) = [] .
	eq take(s(s(s(0))),cons(X,[])) = cons(X,[]) .
	eq take(s(s(s(0))),cons(Y,[])) = cons(Y,[]) .
	eq take(s(s(s(0))),cons(Z,[])) = cons(Z,[]) .
	eq take(s(s(s(0))),cons(X,cons(Y,[]))) = cons(X,cons(Y,[])) .
	eq take(s(s(s(0))),cons(X,cons(Z,[]))) = cons(X,cons(Z,[])) .
	eq take(s(s(s(0))),cons(Y,cons(X,[]))) = cons(Y,cons(X,[])) .
	eq take(s(s(s(0))),cons(Y,cons(Z,[]))) = cons(Y,cons(Z,[])) .
	eq take(s(s(s(0))),cons(Z,cons(X,[]))) = cons(Z,cons(X,[])) .
	eq take(s(s(s(0))),cons(Z,cons(Y,[]))) = cons(Z,cons(Y,[])) .
	eq take(s(s(s(0))),cons(X,cons(Y,cons(Z,[])))) = cons(X,cons(Y,cons(Z,[]))) .
	eq take(s(s(s(0))),cons(X,cons(Z,cons(Y,[])))) = cons(X,cons(Z,cons(Y,[]))) .
	eq take(s(s(s(0))),cons(Y,cons(X,cons(Z,[])))) = cons(Y,cons(X,cons(Z,[]))) .
	eq take(s(s(s(0))),cons(Y,cons(Z,cons(X,[])))) = cons(Y,cons(Z,cons(X,[]))) .
	eq take(s(s(s(0))),cons(Z,cons(X,cons(Y,[])))) = cons(Z,cons(X,cons(Y,[]))) .
	eq take(s(s(s(0))),cons(Z,cons(Y,cons(X,[])))) = cons(Z,cons(Y,cons(X,[]))) .
	eq take(s(s(s(0))),cons(X,cons(Y,cons(Z,cons(X,[]))))) = cons(X,cons(Y,cons(Z,[]))) .
	eq take(s(s(s(0))),cons(X,cons(Z,cons(Y,cons(X,[]))))) = cons(X,cons(Z,cons(Y,[]))) .
	eq take(s(s(s(0))),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,cons(X,cons(Z,[]))) .
	eq take(s(s(s(0))),cons(Y,cons(Z,cons(X,cons(Y,[]))))) = cons(Y,cons(Z,cons(X,[]))) .
	eq take(s(s(s(0))),cons(Z,cons(X,cons(Y,cons(Z,[]))))) = cons(Z,cons(X,cons(Y,[]))) .
	eq take(s(s(s(0))),cons(Z,cons(Y,cons(X,cons(Z,[]))))) = cons(Z,cons(Y,cons(X,[]))) .
	eq take(s(s(s(s(0)))),[]) = [] .
	eq take(s(s(s(s(0)))),cons(X,[])) = cons(X,[]) .
	eq take(s(s(s(s(0)))),cons(Y,[])) = cons(Y,[]) .
	eq take(s(s(s(s(0)))),cons(Z,[])) = cons(Z,[]) .
	eq take(s(s(s(s(0)))),cons(X,cons(Y,[]))) = cons(X,cons(Y,[])) .
	eq take(s(s(s(s(0)))),cons(X,cons(Z,[]))) = cons(X,cons(Z,[])) .
	eq take(s(s(s(s(0)))),cons(Y,cons(X,[]))) = cons(Y,cons(X,[])) .
	eq take(s(s(s(s(0)))),cons(Y,cons(Z,[]))) = cons(Y,cons(Z,[])) .
	eq take(s(s(s(s(0)))),cons(Z,cons(X,[]))) = cons(Z,cons(X,[])) .
	eq take(s(s(s(s(0)))),cons(Z,cons(Y,[]))) = cons(Z,cons(Y,[])) .
	eq take(s(s(s(s(0)))),cons(X,cons(Y,cons(Z,[])))) = cons(X,cons(Y,cons(Z,[]))) .
	eq take(s(s(s(s(0)))),cons(X,cons(Z,cons(Y,[])))) = cons(X,cons(Z,cons(Y,[]))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(X,cons(Z,[])))) = cons(Y,cons(X,cons(Z,[]))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(Z,cons(X,[])))) = cons(Y,cons(Z,cons(X,[]))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(X,cons(Y,[])))) = cons(Z,cons(X,cons(Y,[]))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(Y,cons(X,[])))) = cons(Z,cons(Y,cons(X,[]))) .
	eq take(s(s(s(s(0)))),cons(X,cons(X,cons(Y,cons(Z,[]))))) = cons(X,cons(X,cons(Y,cons(Z,[])))) .
	eq take(s(s(s(s(0)))),cons(X,cons(X,cons(Z,cons(Y,[]))))) = cons(X,cons(X,cons(Z,cons(Y,[])))) .
	eq take(s(s(s(s(0)))),cons(X,cons(Y,cons(X,cons(Z,[]))))) = cons(X,cons(Y,cons(X,cons(Z,[])))) .
	eq take(s(s(s(s(0)))),cons(X,cons(Y,cons(Z,cons(X,[]))))) = cons(X,cons(Y,cons(Z,cons(X,[])))) .
	eq take(s(s(s(s(0)))),cons(X,cons(Z,cons(X,cons(Y,[]))))) = cons(X,cons(Z,cons(X,cons(Y,[])))) .
	eq take(s(s(s(s(0)))),cons(X,cons(Z,cons(Y,cons(X,[]))))) = cons(X,cons(Z,cons(Y,cons(X,[])))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(X,cons(Y,cons(Z,[]))))) = cons(Y,cons(X,cons(Y,cons(Z,[])))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(X,cons(Z,cons(Y,[]))))) = cons(Y,cons(X,cons(Z,cons(Y,[])))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(Y,cons(X,cons(Z,[]))))) = cons(Y,cons(Y,cons(X,cons(Z,[])))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(Y,cons(Z,cons(X,[]))))) = cons(Y,cons(Y,cons(Z,cons(X,[])))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(Z,cons(X,cons(Y,[]))))) = cons(Y,cons(Z,cons(X,cons(Y,[])))) .
	eq take(s(s(s(s(0)))),cons(Y,cons(Z,cons(Y,cons(X,[]))))) = cons(Y,cons(Z,cons(Y,cons(X,[])))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(X,cons(Y,cons(Z,[]))))) = cons(Z,cons(X,cons(Y,cons(Z,[])))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(X,cons(Z,cons(Y,[]))))) = cons(Z,cons(X,cons(Z,cons(Y,[])))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(Y,cons(X,cons(Z,[]))))) = cons(Z,cons(Y,cons(X,cons(Z,[])))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(Y,cons(Z,cons(X,[]))))) = cons(Z,cons(Y,cons(Z,cons(X,[])))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(Z,cons(X,cons(Y,[]))))) = cons(Z,cons(Z,cons(X,cons(Y,[])))) .
	eq take(s(s(s(s(0)))),cons(Z,cons(Z,cons(Y,cons(X,[]))))) = cons(Z,cons(Z,cons(Y,cons(X,[])))) .

endfm


fmod WEAVE is
	sorts MyItem MyList InVec . 
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .

	op weave : MyList MyList -> MyList [metadata "induce"] .

	op in : MyList MyList -> InVec [ctor] .

	vars U V W X Y Z : MyItem .
	var L : MyList .

	eq weave([],[]) = [] .

	eq weave(cons(X,[]),[]) = cons(X,[]) .
	eq weave([],cons(X,[])) = cons(X,[]) .

	eq weave(cons(X,[]),cons(Y,[])) = cons(X,cons(Y,[])) .

	eq weave(cons(X,cons(Y,[])),cons(Z,[])) = cons(X,cons(Z,cons(Y,[]))) .
	eq weave(cons(Z,[]),cons(X,cons(Y,[]))) = cons(Z,cons(X,cons(Y,[]))) .
	


	eq weave([],cons(X,cons(Y,[]))) = cons(X,cons(Y,[])) .
	eq weave(cons(X,cons(Y,[])),[]) = cons(X,cons(Y,[])) .

	eq weave(cons(W,cons(X,[])),cons(Y,cons(Z,[]))) = cons(W,cons(Y,cons(X,cons(Z,[])))) .

endfm


fmod ZIP is 
	sorts MyItem MyList InVec .
	 
	*** DT definitions (constructors)
	op [] : -> MyList [ctor] .
	op cons : MyItem MyList -> MyList [ctor] .
	 
	*** defined function names (to be induced, preds, bk)
	op zip : MyList MyList -> MyList [metadata "induce"] .
	*** input encapsulation
	op in : MyList MyList -> InVec [ctor] .
	 
	vars V W X Y Z : MyItem .

	eq zip([],[]) = [] .
	eq zip([],cons(Y,[])) = cons(Y,[]) .
	eq zip([],cons(Z,[])) = cons(Z,[]) .
	eq zip([],cons(Y,cons(Z,[]))) = cons(Y,cons(Z,[])) .
	eq zip([],cons(Z,cons(Y,[]))) = cons(Z,cons(Y,[])) .
	eq zip(cons(V,[]),[]) = cons(V,[]) .
	eq zip(cons(V,[]),cons(Y,[])) = cons(V,cons(Y,[])) .
	eq zip(cons(V,[]),cons(Z,[])) = cons(V,cons(Z,[])) .
	eq zip(cons(V,[]),cons(Y,cons(Z,[]))) = cons(V,cons(Y,cons(Z,[]))) .
	eq zip(cons(V,[]),cons(Z,cons(Y,[]))) = cons(V,cons(Z,cons(Y,[]))) .
	eq zip(cons(W,[]),[]) = cons(W,[]) .
	eq zip(cons(W,[]),cons(Y,[])) = cons(W,cons(Y,[])) .
	eq zip(cons(W,[]),cons(Z,[])) = cons(W,cons(Z,[])) .
	eq zip(cons(W,[]),cons(Y,cons(Z,[]))) = cons(W,cons(Y,cons(Z,[]))) .
	eq zip(cons(W,[]),cons(Z,cons(Y,[]))) = cons(W,cons(Z,cons(Y,[]))) .
	eq zip(cons(X,[]),[]) = cons(X,[]) .
	eq zip(cons(X,[]),cons(Y,[])) = cons(X,cons(Y,[])) .
	eq zip(cons(X,[]),cons(Z,[])) = cons(X,cons(Z,[])) .
	eq zip(cons(X,[]),cons(Y,cons(Z,[]))) = cons(X,cons(Y,cons(Z,[]))) .
	eq zip(cons(X,[]),cons(Z,cons(Y,[]))) = cons(X,cons(Z,cons(Y,[]))) .
	eq zip(cons(V,cons(W,[])),[]) = cons(V,cons(W,[])) .
	eq zip(cons(V,cons(W,[])),cons(Y,[])) = cons(V,cons(Y,cons(W,[]))) .
	eq zip(cons(V,cons(W,[])),cons(Z,[])) = cons(V,cons(Z,cons(W,[]))) .
	eq zip(cons(V,cons(W,[])),cons(Y,cons(Z,[]))) = cons(V,cons(Y,cons(W,cons(Z,[])))) .
	eq zip(cons(V,cons(W,[])),cons(Z,cons(Y,[]))) = cons(V,cons(Z,cons(W,cons(Y,[])))) .
	eq zip(cons(V,cons(X,[])),[]) = cons(V,cons(X,[])) .
	eq zip(cons(V,cons(X,[])),cons(Y,[])) = cons(V,cons(Y,cons(X,[]))) .
	eq zip(cons(V,cons(X,[])),cons(Z,[])) = cons(V,cons(Z,cons(X,[]))) .
	eq zip(cons(V,cons(X,[])),cons(Y,cons(Z,[]))) = cons(V,cons(Y,cons(X,cons(Z,[])))) .
	eq zip(cons(V,cons(X,[])),cons(Z,cons(Y,[]))) = cons(V,cons(Z,cons(X,cons(Y,[])))) .
	eq zip(cons(W,cons(V,[])),[]) = cons(W,cons(V,[])) .
	eq zip(cons(W,cons(V,[])),cons(Y,[])) = cons(W,cons(Y,cons(V,[]))) .
	eq zip(cons(W,cons(V,[])),cons(Z,[])) = cons(W,cons(Z,cons(V,[]))) .
	eq zip(cons(W,cons(V,[])),cons(Y,cons(Z,[]))) = cons(W,cons(Y,cons(V,cons(Z,[])))) .
	eq zip(cons(W,cons(V,[])),cons(Z,cons(Y,[]))) = cons(W,cons(Z,cons(V,cons(Y,[])))) .
	eq zip(cons(W,cons(X,[])),[]) = cons(W,cons(X,[])) .
	eq zip(cons(W,cons(X,[])),cons(Y,[])) = cons(W,cons(Y,cons(X,[]))) .
	eq zip(cons(W,cons(X,[])),cons(Z,[])) = cons(W,cons(Z,cons(X,[]))) .
	eq zip(cons(W,cons(X,[])),cons(Y,cons(Z,[]))) = cons(W,cons(Y,cons(X,cons(Z,[])))) .
	eq zip(cons(W,cons(X,[])),cons(Z,cons(Y,[]))) = cons(W,cons(Z,cons(X,cons(Y,[])))) .
	eq zip(cons(X,cons(V,[])),[]) = cons(X,cons(V,[])) .
	eq zip(cons(X,cons(V,[])),cons(Y,[])) = cons(X,cons(Y,cons(V,[]))) .
	eq zip(cons(X,cons(V,[])),cons(Z,[])) = cons(X,cons(Z,cons(V,[]))) .
	eq zip(cons(X,cons(V,[])),cons(Y,cons(Z,[]))) = cons(X,cons(Y,cons(V,cons(Z,[])))) .
	eq zip(cons(X,cons(V,[])),cons(Z,cons(Y,[]))) = cons(X,cons(Z,cons(V,cons(Y,[])))) .
	eq zip(cons(X,cons(W,[])),[]) = cons(X,cons(W,[])) .
	eq zip(cons(X,cons(W,[])),cons(Y,[])) = cons(X,cons(Y,cons(W,[]))) .
	eq zip(cons(X,cons(W,[])),cons(Z,[])) = cons(X,cons(Z,cons(W,[]))) .
	eq zip(cons(X,cons(W,[])),cons(Y,cons(Z,[]))) = cons(X,cons(Y,cons(W,cons(Z,[])))) .
	eq zip(cons(X,cons(W,[])),cons(Z,cons(Y,[]))) = cons(X,cons(Z,cons(W,cons(Y,[])))) .
	eq zip(cons(V,cons(W,cons(X,[]))),[]) = cons(V,cons(W,cons(X,[]))) .
	eq zip(cons(V,cons(W,cons(X,[]))),cons(Y,[])) = cons(V,cons(Y,cons(W,cons(X,[])))) .
	eq zip(cons(V,cons(W,cons(X,[]))),cons(Z,[])) = cons(V,cons(Z,cons(W,cons(X,[])))) .
	eq zip(cons(V,cons(W,cons(X,[]))),cons(Y,cons(Z,[]))) = cons(V,cons(Y,cons(W,cons(Z,cons(X,[]))))) .
	eq zip(cons(V,cons(W,cons(X,[]))),cons(Z,cons(Y,[]))) = cons(V,cons(Z,cons(W,cons(Y,cons(X,[]))))) .
	eq zip(cons(V,cons(X,cons(W,[]))),[]) = cons(V,cons(X,cons(W,[]))) .
	eq zip(cons(V,cons(X,cons(W,[]))),cons(Y,[])) = cons(V,cons(Y,cons(X,cons(W,[])))) .
	eq zip(cons(V,cons(X,cons(W,[]))),cons(Z,[])) = cons(V,cons(Z,cons(X,cons(W,[])))) .
	eq zip(cons(V,cons(X,cons(W,[]))),cons(Y,cons(Z,[]))) = cons(V,cons(Y,cons(X,cons(Z,cons(W,[]))))) .
	eq zip(cons(V,cons(X,cons(W,[]))),cons(Z,cons(Y,[]))) = cons(V,cons(Z,cons(X,cons(Y,cons(W,[]))))) .
	eq zip(cons(W,cons(V,cons(X,[]))),[]) = cons(W,cons(V,cons(X,[]))) .
	eq zip(cons(W,cons(V,cons(X,[]))),cons(Y,[])) = cons(W,cons(Y,cons(V,cons(X,[])))) .
	eq zip(cons(W,cons(V,cons(X,[]))),cons(Z,[])) = cons(W,cons(Z,cons(V,cons(X,[])))) .
	eq zip(cons(W,cons(V,cons(X,[]))),cons(Y,cons(Z,[]))) = cons(W,cons(Y,cons(V,cons(Z,cons(X,[]))))) .
	eq zip(cons(W,cons(V,cons(X,[]))),cons(Z,cons(Y,[]))) = cons(W,cons(Z,cons(V,cons(Y,cons(X,[]))))) .
	eq zip(cons(W,cons(X,cons(V,[]))),[]) = cons(W,cons(X,cons(V,[]))) .
	eq zip(cons(W,cons(X,cons(V,[]))),cons(Y,[])) = cons(W,cons(Y,cons(X,cons(V,[])))) .
	eq zip(cons(W,cons(X,cons(V,[]))),cons(Z,[])) = cons(W,cons(Z,cons(X,cons(V,[])))) .
	eq zip(cons(W,cons(X,cons(V,[]))),cons(Y,cons(Z,[]))) = cons(W,cons(Y,cons(X,cons(Z,cons(V,[]))))) .
	eq zip(cons(W,cons(X,cons(V,[]))),cons(Z,cons(Y,[]))) = cons(W,cons(Z,cons(X,cons(Y,cons(V,[]))))) .
	eq zip(cons(X,cons(V,cons(W,[]))),[]) = cons(X,cons(V,cons(W,[]))) .
	eq zip(cons(X,cons(V,cons(W,[]))),cons(Y,[])) = cons(X,cons(Y,cons(V,cons(W,[])))) .
	eq zip(cons(X,cons(V,cons(W,[]))),cons(Z,[])) = cons(X,cons(Z,cons(V,cons(W,[])))) .
	eq zip(cons(X,cons(V,cons(W,[]))),cons(Y,cons(Z,[]))) = cons(X,cons(Y,cons(V,cons(Z,cons(W,[]))))) .
	eq zip(cons(X,cons(V,cons(W,[]))),cons(Z,cons(Y,[]))) = cons(X,cons(Z,cons(V,cons(Y,cons(W,[]))))) .
	eq zip(cons(X,cons(W,cons(V,[]))),[]) = cons(X,cons(W,cons(V,[]))) .
	eq zip(cons(X,cons(W,cons(V,[]))),cons(Y,[])) = cons(X,cons(Y,cons(W,cons(V,[])))) .
	eq zip(cons(X,cons(W,cons(V,[]))),cons(Z,[])) = cons(X,cons(Z,cons(W,cons(V,[])))) .
	eq zip(cons(X,cons(W,cons(V,[]))),cons(Y,cons(Z,[]))) = cons(X,cons(Y,cons(W,cons(Z,cons(V,[]))))) .
	eq zip(cons(X,cons(W,cons(V,[]))),cons(Z,cons(Y,[]))) = cons(X,cons(Z,cons(W,cons(Y,cons(V,[]))))) .

endfm