proposition: Theorem gfp_finite_t : { n | forall x y, gfp x y <-> i n x y }.
proof: Proof. Proof using i_dup i_decr i_dec i_S gfp_reached HF6 HF5 HF0. destruct finite_t_weak_dec_rels with (1 := HF6) as (mR & HmR). exists (S (length mR)). set (l := map i (list_an 0 (S (length mR)))). apply (@gfp_reached (S (length mR))). destruct php_upto with (R := fun R T => forall x y, R x y <-> T x y) (l := l) (m := mR) as (a & R & b & T & c & H1 & H2). + intros R S H ? ?; rewrite H; tauto. + intros R S T H1 H2 ? ?; rewrite H1, H2; tauto. + intros R HR. unfold l in HR; apply in_map_iff in HR. destruct HR as (n & <- & _). destruct (HmR (i n)) as (T & H1 & H2). * intros x y; destruct (i_dec n x y); tauto. * exists T; auto. + unfold l; rewrite map_length, list_an_length; auto. + unfold l in H1; apply map_duplicate_inv in H1. destruct H1 as (a' & n & b' & m & c' & H1 & H3 & H4 & H5 & H6 & H7). exists n, m; rewrite <- H3, <- H5; split; try (intros ? ?; apply H2). apply list_an_duplicate_inv in H7; lia. Qed.
imports: List Arith Nat Lia Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite php) Undecidability.FOL.TRAKHTENBROT(notations)