I have the following program in Dafny:predicate Q (x:int,y:int){x == y}function F (j:int,s:seq<i