@type 'a list 

@function nil: 'a list
@function cons: 'a, 'a list -> 'a list

@function first: 'a list -> 'a
@function rest: 'a list -> 'a list

@function append: 'a list, 'a list -> 'a list
@function reverse: 'a list -> 'a list

@axiom F1: all h:'a. all t: 'a list. 
            first(cons(h,t)) = h

@axiom R1: all h:'a. all t: 'a list. 
            rest(cons(h,t)) = t

@axiom A: all l: 'a list.  
            not(l = nil) ==>  l = cons(first(l), rest(l))

@axiom AppNil: all l1: 'a list.
           append(l1, nil) = l1

@axiom NilApp: all l1: 'a list.
           append(nil, l1) = l1

@axiom AppCons: all h: 'a. all t, l2: 'a list. 
	   append(cons(h,t),l2) = cons(h, append(t,l2))

@axiom RevNil: reverse(nil) = nil
@axiom RevCons: all h: 'a. all l1: 'a list.
            reverse(cons(h,l1)) = append(reverse(l1),cons(h,nil))

@axiom RevRev: all l : 'a list. reverse(reverse(l)) = l

@axiom RevApp: all l1, l2 : 'a list.
           reverse(append(l1,l2)) = append(reverse(l2),reverse(l1))

@axiom Assoc: all l1, l2, l3: 'a list.
           append(append(l1,l2),l3) = append(l1,append(l2,l3))

@requires true
@ensures  out = reverse(inp)
@program  
	  @var inp, out, temp: int list
	  out = nil;
          temp = inp;

          @invariant inp = append(reverse(out), temp)

	  while (not(temp=nil)) {
		out = cons(first(temp), out);
		temp = rest(temp);
	  }
@end
--