class List {

  // container for the list's elements
  var a: array<int>;
  // size of the list
  var size: nat;

  constructor init(len:int)
  {
    a := new int[len];
    size := 0;
  }

  method snoc(e: int)
  {
    a[size] := e;    
    size := size + 1;    
  }

  method tail()    
  {    
    forall (i | 0 <= i < size-2 ) {
      a[i] := a[i + 2];  
    }
    size := size - 1;
  }
  
  method head() returns (h:int)
  {
    h := a[0] ;
  }
  
  method Main() 
  {
    var list := new List.init(4);
    var aux : int;  
    
    list.snoc(2);
    aux := list.head();
    assert (aux == 2) ;    
    
    list.snoc(3);    
    list.snoc(4);
    aux := list.head();    
    assert (aux == 2) ;
    
    list.tail() ;
    aux := list.head();
    assert aux == 3 ;
  }
}