Supermarket Trolley

The Scenario

• Push → forwards; pull → backwards; both → spins
• Concurrent events with cumulative and canceling effects

• Push at time 0; pull at time 1; both at time 2

• 47 axioms and the conjecture

Results

• Easy to prove ...
  
  • Not spinning at time 1
  • Backwards at time 2
  • Not forwards at time 3
  • Spinning at time 3
  • etc