proposition: Theorem size_change_termination {k} (n : nat) (T : fin n -> relation (k_tuple_type k)) (graphs : fin n -> graph k) (approx : forall f, approximates (graphs f) (T f)) (S : list (graph k)) (Strans : is_transitive_closure (fin_list graphs) S) (haspow : forall G, In G S -> exists n f, power_graph_n n G f = Some (true, f)) : well_founded (fin_union T).
proof: Proof. apply size_change_wf_fam with graphs S (TI k); auto. - apply TI_AlmostFull. - intros. specialize (haspow G H). destruct Strans. refine (sct_power_check G (graph_relation G) _ haspow x y _ _). red. firstorder. intuition. intuition. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect