Cacher is the code snippet organizer for pro developers

let incoming_wrong_sequence_number (state) =
  match state.incoming_fix_msg with
  | Some ( ValidMsg msg ) -> 
    let expected_seqn = state.incoming_seq_num + 1 in
    let msg_seqn = msg.full_msg_header.h_msg_seq_num in 
    msg_seqn > expected_seqn
  | _ -> false

let incoming_not_a_sequence_reset ( state ) =
  match state.incoming_fix_msg with
  | Some ( ValidMsg msg ) -> (
    match msg.full_msg_data with
    | Full_FIX_Admin_Msg (Full_Msg_Sequence_Reset _ ) -> false
    | _ -> true )
  | _ -> true
  
let incoming_not_a_poss_duplicate ( state ) =
  match state.incoming_fix_msg with
  | Some ( ValidMsg msg ) -> (
    match msg.full_msg_header.h_poss_dup_flag with 
    | None -> true | Some f -> not (f) )
  | _ -> false
  
theorem out_of_seq_leads_to_gapdetected ( state ) =
  let state' = one_step ( state ) in
  (  state.fe_curr_mode = ActiveSession
  && state.incoming_int_msg = None
  && incoming_wrong_sequence_number state
  && incoming_not_a_sequence_reset  state
  && incoming_not_a_poss_duplicate  state
  )
  ==> (state'.fe_curr_mode = GapDetected)