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