%% Tasks 1,2 nat : type. %name nat N. 0 : nat. s : nat -> nat. plus : nat -> nat -> nat -> type. plus/0 : plus 0 N N. plus/s : plus (s N) M (s P) <- plus N M P. list : nat -> type. nil : list 0. cons : nat -> list N -> list (s N). append : list N -> list M -> plus N M P -> list P -> type. %mode append +X1 +X2 +X3 -X4. append/nil : append nil L plus/0 L. append/cons : append (cons X L) L' (plus/s Dplus) (cons X L'') <- append L L' Dplus L''. %worlds () (append _ _ _ _). %total L (append L _ _ _). %% non-indexed trees tree : type. leaf : tree. node : nat -> tree -> tree -> tree. nelts : tree -> nat -> type. %% You fill in! flatten : {T:tree} nelts T N -> list N -> type. %mode flatten +T +X1 -X2. %% You fill in! %worlds () (flatten _ _ _). %total T (flatten T _ _).