lemma MapDistributivity(xs:seq<int>, f:int->int, g:int->int)
   requires forall x :: x in xs ==> f.requires(x);
   requires forall x :: x in xs ==> g.requires(f(x));
   ensures forall x :: x in MapSeq(xs,f) ==> g.requires(x);
   ensures MapSeq(MapSeq(xs,f), g) == MapSeq(xs, Compose(f,g));
{
   if xs != []
   {
     MapDistributivity(xs[1..], f, g);
   }
}
 
function Compose(f:int->int, g:int->int) : int->int
{
  x
    reads f.reads(x)
    reads if f.requires(x) then g.reads(f(x)) else {} 
    requires f.requires(x) 
    requires g.requires(f(x)) 
      -> g(f(x))
}
 
function MapSeq(xs:seq<int>, f:int->int) : seq<int>
   reads MapSeqReads(xs, f);
   requires forall x :: x in xs ==> f.requires(x);
   ensures |xs| == |MapSeq(xs,f)|;
   ensures forall x :: x in xs ==> f(x) in MapSeq(xs,f); 
{
  if xs == [] then []
  else [f(xs[0])] + MapSeq(xs[1..], f) 
}
 
function MapSeqReads(xs:seq<int>, f:int->int) : set<object>
   reads if |xs| > 0 then f.reads(xs[0]) + MapSeqReads(xs[1..], f) else {};
   decreases xs;
   ensures forall x :: x in xs ==> f.reads(x) <= MapSeqReads(xs,f); 
{
  if xs == [] then {}
  else f.reads(xs[0]) + MapSeqReads(xs[1..],f)
}