let f (n: int) : int = 
  n+6


let g (n: int) : int =
  n*2


let h (n: int) : int =
  n+3


let rec double (n: int) : int =
  if n = 0 then 0
  else 2 + double (n-1)

let rec cat xs ys =
    match xs with
    | [] -> ys
    | hd::tl -> hd :: cat tl ys

let rec sumrec (n: int) : int =
  if n = 0 then 0
  else n + sumrec(n-1)


let sumform (n: int) : int =
  n * (n+1) / 2

(* 
Proposed theorems:
f (g x) == g (h x)
double x == x*2 
cat (cat xs ys) zs == cat xs (cat ys zs)
sumrec x == sumform x
*)

(* clearly this testing is insufficient as proof. we must do better! *)
let _ =
  assert ( f(g 0) = g(h 0) );
  assert ( f(g 1) = g(h 1) );
  assert ( f(g 2) = g(h 2) );
  assert ( f(g 10) = g(h 10) );
  assert ( f(g 1024) = g(h 1024) );
  assert ( f(g 123456789) = g(h 123456789) );
  
  assert ( double 0 = (0*2) );
  assert ( double 1 = (1*2) );
  assert ( double 10 = (10*2) );
  assert ( double 1234 = (1234*2) );
  assert ( double 9999 = (9999*2) );
  
  assert ( sumrec 0 = sumform 0 );
  assert ( sumrec 1 = sumform 1 );
  assert ( sumrec 2 = sumform 2 );
  assert ( sumrec 10 = sumform 10 );
  assert ( sumrec 100 = sumform 100 );
  assert ( sumrec 1000 = sumform 1000 )