begin
 down x1 . [][] <->x1 ;  { transitivity } 
 [] down x1 . <> true ;  { irreflexivity }
 <>true                  { initial successor }
end