mmaroti

I think you need more assumptions. This satisfies your requirements:

X(0) = 0000, Y(a) = 0001, X(a) = 0011, Y(2a)= 0111.

This is blatantly false. People are using formal verification tools in hardware design, and they do work and they do compose. Here is a simple verilog code which accomplishes some of what he wants.

  module Blinker (
   input wire clock,
   output reg state
  );
  
  always @(posedge clock)
   state <= !state;
  
  `if FORMAL
  
  always @(posedge clock)
   assert ($past(state) != state);
  
  `endif
  
  endmodule
  
  module testbench (
   input wire clock,
   output wire state1,
   output wire state2
  );
  
  Blinker blinker1(clock, state1);
  Blinker blinker2(clock, state2);
  
  `if FORMAL
  
  # assume that they are different
  assume (state1 != state2);
  
  # then they stay different
  always @(posedge clock)
    assert (state1 != state2);
  
  `endif
  
  endmodule

Moral of the story: broken spec cannot be used, and I am saying this as a mathematician!

I am a researcher, and I fail to find detailed data, please help! In all datasets we see cumulative confirmed, recovered and death numbers organized by day. We would need culumative confirmed by onset time (first symptoms), and confirmed by test time (the current value). We would also need recovered and death by onset time and confirmation time. Where are these numbers?

You can use the tensor formalism to express combinatorial problems, but these will not be smooth, so gradient descent algorithms will not work. However, you can turn such boolean tensor problems into huge SAT problems and solve them with SAT solvers. See for example here: https://github.com/mmaroti/uasat

There are a ton of other competing technologies. We have been to the Microsoft Indoor Localization Competition and saw the estimote there too:

http://research.microsoft.com/en-us/events/indoorloccompetit...

The 4 meter precision is in the middle of the pack.