proposition: Lemma big_wf_a p a (f : nat -> option nat) : (forall p' a', f p' = Some a' -> forall n, reaches_plus (p', (n+a', 0)) (p, (n+a, 0))) -> terminating (p, (a, 0)) + non_terminating (p, (a, 0)) + { '(p', (a', b')) | reaches (p, (a, 0)) (p', (a', b')) /\ a' <= l /\ b' <= l }.
proof: Proof. elim /(well_founded_induction_type wf_R) : f p a. move=> f IH p a Hf. have [[Hp|[[p' a'] Hp]]|[[p' [a' b']] [Hp ?]]] := next_waypoint_a p a. - left. by left. - have /= ? := reaches_plus_state_bound (Hp 0). set P := (_ + _ + _)%type. have HR : R (update f p (Some a)) f -> P. { move=> /IH /(_ p' a') /=. case; [|case|]. - move=> p''' a'''. rewrite /update. case: (Nat.eq_dec p''' p). { by move=> -> [<-]. } move=> ? /Hf Hp''' n. by apply: (reaches_plus_trans (Hp''' n) (Hp n)). - move=> /reaches_terminating Hp'. left. left. by apply /Hp' /reaches_plus_incl /(Hp 0). - move=> /reaches_non_terminating Hp'. left. right. by apply /Hp' /reaches_plus_incl /(Hp 0). - move=> [[p''' [a''' b''']]] [Hp'] ?. right. exists (p''', (a''', b''')). split; last done. by apply: (reaches_trans (reaches_plus_incl (Hp 0))). } case H'p: (f p) => [a''|]. + case E: (a''-a) => [|?]. { left. right. move: H'p => /Hf{Hf} H'p. apply: (reaches_non_terminating' (reaches_plus_incl (H'p 0))). apply: (loop_a _ H'p). lia. } apply /HR /(R_Some a''); [done|done|lia]. + by apply /HR /R_None. - right. by exists (p', (a', b')). Qed.
imports: List ssrfun List PeanoNat Lia Operators_Properties ssreflect ssrbool ssrfun