fun Z () = 0; fun S n = n+1; fun pr_1_1 x:int = x; fun pr_1_2 (x:int,y:int) = x; fun pr_2_2 (x:int,y:int) = y; fun pr_1_3 (x:int, y:int, z:int) = x; fun pr_2_3 (x:int, y:int, z:int) = y; fun pr_3_3 (x:int, y:int, z:int) = z; fun compose_1 (g1,h) x = h (g1 x); fun compose_2 (g1,g2,h) x = h (g1 x) (g2 x ); fun compose_3 (g1,g2,g3,h) x = h (g1 x) ( g2 x) (g3 x); fun pr_rek_1 (g,h) y = if (y=0) then g () else h (y-1,pr_rek_1 (g,h) (y-1) ); fun pr_rek_2 (g,h) x1 y = if (y=0) then g x1 else h (x1,y-1,pr_rek_2 (g,h) x1 (y-1) ); fun pr_rek_3 g h x1 x2 y = if (y=0) then g x1 x2 else h x1 x2 (y-1) (pr_rek_3 g h x1 x2 (y-1) ); val c_1_0 = compose_1 (Z,S); val c_2_0 = compose_1 (c_1_0,S); val c_3_0 = compose_1 (c_2_0,S); val c_0_1 = pr_rek_1 (Z, pr_2_2); val c_1_1 = pr_rek_1 (c_1_0, pr_2_2); val c_2_1 = pr_rek_1 (c_2_0, pr_2_2); val c_3_1 = pr_rek_1 (c_3_0, pr_2_2); val c_0_2 = compose_1 (pr_1_2,c_0_1); val c_1_2 = compose_1 (pr_1_2,c_1_1); val c_2_2 = compose_1 (pr_1_2,c_2_1); val c_3_2 = compose_1 (pr_1_2,c_2_1); val add = pr_rek_2 (pr_1_1,compose_1 (pr_3_3,S)); val add = function (x,y) -> x+y; val mult = pr_rek_2 (c_0_1,compose_2 (pr_1_3,pr_3_3,add));