proposition: Lemma small_decider p a b L : a <= l -> b <= l -> Forall (fun '(p', (a', b')) => reaches_plus (p', (a', b')) (p, (a, b)) /\ p' < l /\ a' <= l /\ b' <= l ) L -> NoDup L -> terminating (p, (a, b)) + non_terminating (p, (a, b)).
proof: Proof. move Hn: ((l*(l+1)*(l+1)+1) - length L) => n. elim: n L Hn p a b. { move=> L ? ????? H1L /NoDup_incl_length H2L. have : incl L (list_prod (seq 0 l) (list_prod (seq 0 (l+1)) (seq 0 (l+1)))). { move=> [p [a b]]. move: H1L => /Forall_forall H1L /H1L ?. apply /in_prod; [|apply /in_prod]; apply /in_seq; lia. } move=> /H2L. rewrite ?prod_length ?seq_length. lia. } move=> n IH L ? p a b ? ? H1L H2L. have [[|]|[[p' [a' b']] [Hp ?]]] := next_small_waypoint p a b; [tauto|tauto|]. have := In_dec _ (p, (a, b)) L. case. { do ? decide equality. } - move=> H'p. right. apply: reaches_plus_self_loop. by move: H1L H'p => /Forall_forall H /H []. - move=> H'p. have := (IH ((p, (a, b)) :: L) _ p' a' b'). case. + move=> /=. lia. + lia. + lia. + constructor. * split; first done. move: Hp => /reaches_plus_state_bound /=. lia. * apply: Forall_impl H1L. move=> [p'' [a'' b'']] [? ?]. split; last done. by apply: (reaches_plus_reaches _ (reaches_plus_incl Hp)). + by constructor. + move=> /reaches_terminating H. left. by apply /H /reaches_plus_incl. + move=> /reaches_non_terminating H. right. by apply /H /reaches_plus_incl. Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun