_____ _ | ___(_)_ ____ __ | |_ | | '_ \ \ / / | _| | | | | \ V / |_| |_|_| |_|\_/
Program:
datatype bool ::= true | false. datatype nat ::= 0 | s(nat). datatype list(A) ::= nil | (A : list(A)). type [A] ::= list(A). add :: nat -> nat -> nat. add(0,X):=X. add(s(X),Y):=s(add(X,Y)). incL :: [nat] -> nat -> [nat]. incL([],_):=[]. incL(X:L,I):=add(X,I):incL(L,I). prod :: nat -> nat -> nat. prod(0,X):=X. prod(s(X),Y):=add(Y,prod(X,Y)).
Function:
Inversion parameters: