KKostya
7/26/2018 - 2:22 PM

no_moving_back_proved.ml

no_moving_back_proved.ml
content_copyfile_download
theorem never_goes_back state = 
  state.incoming <> None
  ==>
  no_moving_back (one_step state).outgoing